aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/ltac2.v
blob: d66fb6808d206abaab201f1b7c31c41a1490afdb (plain)
1
2
3
4
5
6
(* Check that Match arguments are forbidden *)
Ltac E x := apply x.
Goal True -> True.
Fail E ltac:(match goal with
        |  |- _ => intro H
        end).