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