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

4 files changed, 16 insertions, 23 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index d5053dc82..0a486cb1e 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -90,10 +90,10 @@ GEXTEND Gram
       | IDENT "Go"; IDENT "next" -> VernacGo GoNext
       | IDENT "Guarded" -> VernacCheckGuard
 (* Hints for Auto and EAuto *)
-      | IDENT "Create"; local = locality; IDENT "HintDb" ; 
+      | IDENT "Create"; IDENT "HintDb" ; 
 	  id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
-	    VernacCreateHintDb (enforce_locality_of local, id, b)
-      | IDENT "Hint"; local = locality; h = hint;
+	    VernacCreateHintDb (use_locality (), id, b)
+      | IDENT "Hint"; local = obsolete_locality; h = hint;
         dbnames = opt_hintbases ->
 	  VernacHints (enforce_locality_of local,dbnames, h)
 	  
@@ -104,7 +104,7 @@ GEXTEND Gram
 	    [Genarg.in_gen Genarg.rawwit_constr c])
       ] ];
 
-  locality:
+  obsolete_locality:
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
   hint:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 57c2ef677..4b79113f3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -114,13 +114,6 @@ GEXTEND Gram
   ;
 END
 
-GEXTEND Gram
-  GLOBAL: locality non_locality;
-  locality:
-    [ [ IDENT "Local" -> true | -> false ] ]
-  ;
-END
-
 let test_plurial_form = function
   | [(_,([_],_))] ->
       Flags.if_verbose warning
@@ -789,10 +782,10 @@ GEXTEND Gram
   GLOBAL: syntax;
 
   syntax:
-   [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT -> 
+   [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> 
          VernacOpenCloseScope (enforce_locality_of local,true,sc)
 
-     | IDENT "Close"; local = locality; IDENT "Scope"; sc = IDENT -> 
+     | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> 
          VernacOpenCloseScope (enforce_locality_of local,false,sc)
 
      | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
@@ -805,16 +798,17 @@ GEXTEND Gram
        "["; scl = LIST0 opt_scope; "]" -> 
 	 VernacArgumentsScope (use_non_locality (),qid,scl)
 
-     | IDENT "Infix"; local = locality;
+     | IDENT "Infix"; local = obsolete_locality;
 	 op = ne_string; ":="; p = global; 
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
          VernacInfix (enforce_locality_of local,(op,modl),p,sc)
-     | IDENT "Notation"; local = locality; id = identref; idl = LIST0 ident; 
-	 ":="; c = constr;
+     | IDENT "Notation"; local = obsolete_locality; id = identref; 
+	 idl = LIST0 ident; ":="; c = constr;
 	 b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
            VernacSyntacticDefinition (id,(idl,c),enforce_locality_of local,b)
-     | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr;
+     | IDENT "Notation"; local = obsolete_locality; s = ne_string; ":="; 
+	 c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
            VernacNotation (enforce_locality_of local,c,(s,modl),sc)
@@ -823,7 +817,8 @@ GEXTEND Gram
 	 pil = LIST1 production_item; ":="; t = Tactic.tactic
          -> VernacTacticNotation (n,pil,t)
 
-     | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; 
+     | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; 
+	 s = ne_string; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
 	 -> VernacSyntaxExtension (enforce_locality_of local,(s,l))
 
@@ -831,6 +826,9 @@ GEXTEND Gram
         to factorize with other "Print"-based vernac entries *)
   ] ]
   ;
+  obsolete_locality:
+    [ [ IDENT "Local" -> true | -> false ] ]
+  ;
   tactic_level:
     [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
   ;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index ed4f41c4e..d81727487 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -496,9 +496,6 @@ module Vernac_ =
   struct
     let gec_vernac s = Gram.Entry.create ("vernac:" ^ s)
 
-    let locality = gec_vernac "locality"
-    let non_locality = gec_vernac "non_locality"
-
     (* The different kinds of vernacular commands *)
     let gallina = gec_vernac "gallina"
     let gallina_ext = gec_vernac "gallina_ext"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e089389fe..f084c74f0 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -200,8 +200,6 @@ module Tactic :
 module Vernac_ :
   sig
     open Decl_kinds
-    val locality : bool Gram.Entry.e
-    val non_locality : bool Gram.Entry.e
     val gallina : vernac_expr Gram.Entry.e
     val gallina_ext : vernac_expr Gram.Entry.e
     val command : vernac_expr Gram.Entry.e