diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-02 17:43:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-02 17:43:56 +0000 |
| commit | e895f9ca19247f4fe58833f91e948e200bc9a6e5 (patch) | |
| tree | b6be61c1a3c94e8db8ed2f293ce8ad6b56fbcb6b /test-suite/success/ltac.v | |
| parent | 6342bc95a166d224ea64f1e3b8977e4f3560b485 (diff) | |
Fixing a bug introduced in r12304 (move of interpretation of
Local/Global modifiers in interpretation loop so as to support
Local/Global for grammar extension) that made use of
DuringSyntaxChecking error wrapper inappropriately nested with the
DuringCommandInterp error wrapper, what disturbed the error
processors. Good thing, we can now simplify things and completely
remove the DuringSyntaxChecking wrapper.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13667 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/ltac.v')
| -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 a8d1ba7f5..7387add6a 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. |