diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/ltac.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index a8d1ba7f5a..7387add6a2 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -298,3 +298,7 @@ evar(foo:nat). let evval := eval compute in foo in not_eq evval 1. let evval := eval compute in foo in not_eq 1 evval. Abort. + +(* Check that this returns an error and not an anomaly (see r13667) *) + +Fail Local Tactic Notation "myintro" := intro. |