diff options
| -rw-r--r-- | test-suite/success/ltac.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 1edddcfd74..c4a45b0315 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -298,7 +298,3 @@ 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. |