test-suite/failure/ltac1.v


1
2
3
4
5
6
7
8

(* Check all variables are different in a Context *)
Ltac X := match goal with
          | x:_,x:_ |- _ => apply x
          end.
Goal True -> True -> True.
intros.
Fail X.
Abort.