blob: bd93cdc8584d7481938b6162e521eabf7817b502 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* 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.
|
