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