aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/ltac1.v
blob: 7b496a750ca02d2b50a5b2e9a595d20500e4f15e (plain)
1
2
3
4
5
6
7
(* Check all variables are different in a Context *)
Ltac X := match goal with
          | x:_,x:_ |- _ => apply x
          end.
Goal True -> True -> True.
intros.
X.