diff options
Diffstat (limited to 'test-suite/failure/ltac2.v')
| -rw-r--r-- | test-suite/failure/ltac2.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/failure/ltac2.v b/test-suite/failure/ltac2.v index 14436e58..d66fb680 100644 --- a/test-suite/failure/ltac2.v +++ b/test-suite/failure/ltac2.v @@ -1,6 +1,6 @@ (* Check that Match arguments are forbidden *) Ltac E x := apply x. Goal True -> True. -E ltac:(match goal with +Fail E ltac:(match goal with | |- _ => intro H end). |