From e895f9ca19247f4fe58833f91e948e200bc9a6e5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 2 Dec 2010 17:43:56 +0000
Subject: 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
---
 test-suite/success/ltac.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3