Fixing/improving management of uniform prefix Local and Global

modifiers (added a "Syntax Checking" phase for raising a non
interpretation error just after a dot is parsed -- maybe exaggerated
complication for what we want to do ?).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11783 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 2 deletions

diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 14207b5e5..7f869c166 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -13,6 +13,7 @@ open Util
 open Flags
 open Cerrors
 open Vernac
+open Vernacexpr
 open Pcoq
 open Protectedtoplevel
 
@@ -262,6 +263,7 @@ let rec is_pervasive_exn = function
   | Error_in_file (_,_,e) -> is_pervasive_exn e
   | Stdpp.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
@@ -270,7 +272,8 @@ let rec is_pervasive_exn = function
 let print_toplevel_error exc =
   let (dloc,exc) =
     match exc with
-      | DuringCommandInterp (loc,ie) ->
+      | DuringCommandInterp (loc,ie)
+      | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) ->
           if loc = dummy_loc then (None,ie) else (Some loc, ie)
       | _ -> (None, exc) 
   in
@@ -321,7 +324,8 @@ let rec discard_to_dot () =
  * in encountered. *)
 
 let process_error = function
-  | DuringCommandInterp _ as e -> e
+  | DuringCommandInterp _ 
+  | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e
   | e ->
       if is_pervasive_exn e then 
 	e