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

5 files changed, 9 insertions, 13 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.
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index b90b44687c..3bd9462cef 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -529,8 +529,7 @@ type 'a value =
 
 let eval_call c = 
   let filter_compat_exn = function
-    | Vernac.DuringCommandInterp (loc,inner)
-    | Vernacexpr.DuringSyntaxChecking (loc,inner) -> inner
+    | Vernac.DuringCommandInterp (loc,inner) -> inner
     | Vernacexpr.Quit -> raise Vernacexpr.Quit
     | e -> e
   in
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 7b3acfa619..ddf3ac6575 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -275,7 +275,6 @@ let rec is_pervasive_exn = function
   | Error_in_file (_,_,e) -> is_pervasive_exn e
   | Loc.Exc_located (_,e) -> is_pervasive_exn e
   | DuringCommandInterp (_,e) -> is_pervasive_exn e
-  | DuringSyntaxChecking (_,e) -> is_pervasive_exn e
   | _ -> false
 
 (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
@@ -284,8 +283,7 @@ let rec is_pervasive_exn = function
 let print_toplevel_error exc =
   let (dloc,exc) =
     match exc with
-      | DuringCommandInterp (loc,ie)
-      | DuringSyntaxChecking (loc,ie) ->
+      | DuringCommandInterp (loc,ie) ->
           if loc = dummy_loc then (None,ie) else (Some loc, ie)
       | _ -> (None, exc)
   in
@@ -334,8 +332,7 @@ let rec discard_to_dot () =
  * in encountered. *)
 
 let process_error = function
-  | DuringCommandInterp _
-  | DuringSyntaxChecking _ as e -> e
+  | DuringCommandInterp _ as e -> e
   | e ->
       if is_pervasive_exn e then
 	e
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1df58a10ae..2293707e2d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -33,8 +33,7 @@ exception HasNotFailed
 let raise_with_file file exc =
   let (cmdloc,re) =
     match exc with
-      | DuringCommandInterp(loc,e)
-      | DuringSyntaxChecking(loc,e) -> (loc,e)
+      | DuringCommandInterp(loc,e) -> (loc,e)
       | e -> (dummy_loc,e)
   in
   let (inner,inex) =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 36c2b26c01..797fc79c6c 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -351,10 +351,7 @@ and located_vernac_expr = loc * vernac_expr
 (* Locating errors raised just after the dot is parsed but before the
    interpretation phase *)
 
-exception DuringSyntaxChecking of exn located
-
-let syntax_checking_error loc s =
-  raise (DuringSyntaxChecking (loc,UserError ("",Pp.str s)))
+let syntax_checking_error loc s = user_err_loc (loc,"",Pp.str s)
 
 (**********************************************************************)
 (* Managing locality *)