aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/ltac4.v
blob: 5b0396d164ea43060260775be7b25240b7cfdb6e (plain)
1
2
3
4
5
6
(* Check static globalisation of tactic names *)
(* Proposed by Benjamin (mars 2002) *)
Goal forall n : nat, n = n.
induction n.
Fail try REflexivity.