- Standardized prefix use of "Local"/"Global" modifiers as decided in

  late 2008 Coq WG.
- Updated Copyright file wrt JProver.



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

1 files changed, 40 insertions, 41 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index bcb2f7a57..57c2ef677 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -64,7 +64,13 @@ let default_command_entry =
 let no_hook _ _ = ()
 GEXTEND Gram
   GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode;
-  vernac:
+  vernac: FIRST
+    [ [ IDENT "Time"; locality; v = vernac_aux -> 
+          check_locality (); VernacTime v 
+      | locality; v = vernac_aux -> 
+	  check_locality (); v ] ]
+  ;
+  vernac_aux:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
     [ [ g = gallina; "." -> g 
@@ -74,12 +80,14 @@ GEXTEND Gram
       | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l
     ] ]
   ;
-  vernac: FIRST
-    [ [ IDENT "Time"; v = vernac  -> VernacTime v ] ]
-  ;
-  vernac: LAST  
+  vernac_aux: LAST  
     [ [ prfcom = default_command_entry -> prfcom ] ]
   ;
+  locality:
+    [ [ IDENT "Local" -> locality_flag := Some true
+      | IDENT "Global" -> locality_flag := Some false
+      | -> locality_flag := None ] ]
+  ;
   noedit_mode:
     [ [ c = subgoal_command -> c None] ]
   ;
@@ -109,10 +117,7 @@ END
 GEXTEND Gram
   GLOBAL: locality non_locality;
   locality:
-    [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> false ] ]
-  ;
-  non_locality:
-    [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> true ] ]
+    [ [ IDENT "Local" -> true | -> false ] ]
   ;
 END
 
@@ -196,9 +201,8 @@ GEXTEND Gram
 	no_hook, (Local, Flags.boxed_definitions(), Definition)
       | IDENT "Example" -> 
 	no_hook, (Global, Flags.boxed_definitions(), Example)
-      | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, false, SubClass)
-      | IDENT "Local"; IDENT "SubClass"  ->
-          Class.add_subclass_hook, (Local, false, SubClass) ] ] 
+      | IDENT "SubClass"  ->
+          Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ] 
   ;
   assumption_token:
     [ [ "Hypothesis" -> (Local, Logical)
@@ -463,16 +467,13 @@ GEXTEND Gram
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
-        IDENT "Transparent"; b = non_locality; l = LIST1 global ->
-          VernacSetOpacity (b,[Conv_oracle.transparent,l])
-      | IDENT "Opaque"; b = non_locality; l = LIST1 global ->
-          VernacSetOpacity (b,[Conv_oracle.Opaque, l])
+        IDENT "Transparent"; l = LIST1 global ->
+          VernacSetOpacity (use_non_locality (),[Conv_oracle.transparent,l])
+      | IDENT "Opaque"; l = LIST1 global ->
+          VernacSetOpacity (use_non_locality (),[Conv_oracle.Opaque, l])
       | IDENT "Strategy"; l =
           LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
-            VernacSetOpacity (false,l)
-      | IDENT "Local"; IDENT "Strategy"; l =
-          LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
-            VernacSetOpacity (true,l)
+            VernacSetOpacity (use_locality (),l)
       (* Canonical structure *)
       | IDENT "Canonical"; IDENT "Structure"; qid = global ->
 	  VernacCanonical qid
@@ -485,28 +486,27 @@ GEXTEND Gram
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_global_to_id qid in
-	  VernacDefinition ((Global,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((use_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = coerce_global_to_id qid in
-	  VernacDefinition ((Local,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((enforce_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
-	   VernacIdentityCoercion (Local, f, s, t)
+	   VernacIdentityCoercion (enforce_locality_exp (), f, s, t)
       | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr -> 
-	   VernacIdentityCoercion (Global, f, s, t)
+	   VernacIdentityCoercion (use_locality_exp (), f, s, t)
       | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
 	 s = class_rawexpr; ">->"; t = class_rawexpr -> 
-	  VernacCoercion (Local, qid, s, t)
+	  VernacCoercion (enforce_locality_exp (), qid, s, t)
       | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
-	  VernacCoercion (Global, qid, s, t)
+	  VernacCoercion (use_locality_exp (), qid, s, t)
 	     
       | IDENT "Context"; c = binders_let -> 
 	  VernacContext c
 	    
-      | IDENT "Instance"; local = non_locality; name = identref; 
-	 sup = OPT binders_let; ":";
+      | IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
 	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ; 
 	 props = [ ":="; decl = record_declaration -> decl | -> CRecord (loc, None, []) ] ->
@@ -519,17 +519,15 @@ GEXTEND Gram
 	     let (loc, id) = name in 
 	       (loc, Name id)
 	   in
-	     VernacInstance (not local, sup, (n, expl, t), props, pri)
+	     VernacInstance (not (use_non_locality ()), sup, (n, expl, t), props, pri)
 
       | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
 
       (* Implicit *)
-      | IDENT "Implicit"; IDENT "Arguments"; 
-	   local = [ IDENT "Global" -> false | IDENT "Local" -> true | -> Lib.sections_are_opened () ]; 
-	   qid = global; 
+      | IDENT "Implicit"; IDENT "Arguments"; qid = global; 
 	   pos = OPT [ "["; l = LIST0 implicit_name; "]" -> 
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
-	   VernacDeclareImplicits (local,qid,pos)
+	   VernacDeclareImplicits (use_section_locality (),qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
@@ -792,10 +790,10 @@ GEXTEND Gram
 
   syntax:
    [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT -> 
-         VernacOpenCloseScope (local,true,sc)
+         VernacOpenCloseScope (enforce_locality_of local,true,sc)
 
      | IDENT "Close"; local = locality; IDENT "Scope"; sc = IDENT -> 
-         VernacOpenCloseScope (local,false,sc)
+         VernacOpenCloseScope (enforce_locality_of local,false,sc)
 
      | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc,key)
@@ -803,22 +801,23 @@ GEXTEND Gram
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; 
        refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
 
-     | IDENT "Arguments"; IDENT "Scope"; local = non_locality; qid = global;
-       "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (local,qid,scl)
+     | IDENT "Arguments"; IDENT "Scope"; qid = global;
+       "["; scl = LIST0 opt_scope; "]" -> 
+	 VernacArgumentsScope (use_non_locality (),qid,scl)
 
      | IDENT "Infix"; local = locality;
 	 op = ne_string; ":="; p = global; 
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         VernacInfix (local,(op,modl),p,sc)
+         VernacInfix (enforce_locality_of local,(op,modl),p,sc)
      | IDENT "Notation"; local = locality; id = identref; idl = LIST0 ident; 
 	 ":="; c = constr;
 	 b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
-           VernacSyntacticDefinition (id,(idl,c),local,b)
+           VernacSyntacticDefinition (id,(idl,c),enforce_locality_of local,b)
      | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-           VernacNotation (local,c,(s,modl),sc)
+           VernacNotation (enforce_locality_of local,c,(s,modl),sc)
 
      | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; 
 	 pil = LIST1 production_item; ":="; t = Tactic.tactic
@@ -826,7 +825,7 @@ GEXTEND Gram
 
      | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (local,(s,l))
+	 -> VernacSyntaxExtension (enforce_locality_of local,(s,l))
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)