test-suite/failure/ltac1.v


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.