test-suite/failure/ltac2.v


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).