| products/Sources/formale Sprachen/C/Linux/include/linux/ (Firefox Browser Version 153.0.1©) Datei vom 24.10.2025 mit Größe 3 kB |
|
Quellcode-Bibliothek bug_4966.v Sprache: Coq |
|||||||||||||||
|
(* Interpretation of auto as an argument of an ltac function (i.e. as an ident) was wrongly "auto Axiom proof_admitted : False. #[export] Hint Extern 0 => case proof_admitted : unused. Ltac do_tac tac := tac. Goal False. Set Ltac Profiling. Fail solve [ do_tac auto ]. Abort.
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung: (vorverarbeitet am 2026-09-30) ¤*Bot Zugriff |
|
||||||||||||||
2026-10-10