blob: 55925a7a62739c3d571121f9e08deb0fd27b56c2 (
plain)
1
2
3
4
5
6
|
(* Check that Match arguments are forbidden *)
Tactic Definition E x := Apply x.
Goal True->True.
E (Match Context With [ |- ? ] -> Intro H).
(* Should fail with "Immediate Match producing tactics not allowed in
local definitions" *)
|
