aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/ltac1.v
blob: d0256619060e099e749fa7b15f44e856ec9f7cab (plain)
1
2
3
4
5
(* Check all variables are different in a Context *)
Tactic Definition X := Match Context With [ x:?; x:? |- ? ] -> Apply x.
Goal True->True->True.
Intros.
X.