|
(* Interpretation of auto as an argument of an ltac function (i.e. as an ident) was wrongly "auto with *" *)
Axiom proof_admitted : False.
Hint Extern 0 => case proof_admitted : unused.
Ltac do_tac tac := tac.
Goal False.
Set Ltac Profiling.
Fail solve [ do_tac auto ].
Abort.
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
