New cleaning phase of the Local/Global option management

- Clarification and documentation of the different styles of
  Local/Global modifiers in vernacexpr.ml
- Addition of Global in sections for Open/Close Scope.
- Addition of Local for Ltac when not in sections.

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

4 files changed, 37 insertions, 30 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 7f63428c83..0e97b2a7fd 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -227,6 +227,6 @@ GEXTEND Gram
   Vernac_.command:
     [ [ IDENT "Ltac";
         l = LIST1 tacdef_body SEP "with" ->
-          VernacDeclareTacticDefinition (true, l) ] ]
+          VernacDeclareTacticDefinition (use_module_locality (), true, l) ] ]
   ;
   END
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 90245fa454..39e577b88c 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -92,16 +92,16 @@ GEXTEND Gram
 (* Hints for Auto and EAuto *)
       | IDENT "Create"; IDENT "HintDb" ;
 	  id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
-	    VernacCreateHintDb (use_locality (), id, b)
+	    VernacCreateHintDb (use_module_locality (), id, b)
       | IDENT "Hint"; local = obsolete_locality; h = hint;
 	  dbnames = opt_hintbases ->
-	  VernacHints (enforce_locality_of local,dbnames, h)
+	  VernacHints (enforce_module_locality local,dbnames, h)
 
 (* Declare "Resolve" directly so as to be able to later extend with
    "Resolve ->" and "Resolve <-" *)
       | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural;
 	  dbnames = opt_hintbases ->
-	  VernacHints (enforce_locality_of false,dbnames,
+	  VernacHints (use_module_locality (),dbnames,
 	    HintsResolve (List.map (fun x -> (n, true, x)) lc))
 
 (*This entry is not commented, only for debug*)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 28a66182ca..e1a71ff23f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -83,8 +83,8 @@ GEXTEND Gram
     [ [ prfcom = default_command_entry -> prfcom ] ]
   ;
   locality:
-    [ [ IDENT "Local" -> locality_flag := Some true
-      | IDENT "Global" -> locality_flag := Some false
+    [ [ IDENT "Local" -> locality_flag := Some (loc,true)
+      | IDENT "Global" -> locality_flag := Some (loc,false)
       | -> locality_flag := None ] ]
   ;
   noedit_mode:
@@ -490,19 +490,19 @@ GEXTEND Gram
 	  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_reference_to_id qid in
-	  VernacDefinition ((enforce_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((enforce_locality_exp true,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 (enforce_locality_exp (), f, s, t)
+	   VernacIdentityCoercion (enforce_locality_exp true, f, s, t)
       | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr ->
 	   VernacIdentityCoercion (use_locality_exp (), f, s, t)
       | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
 	 s = class_rawexpr; ">->"; t = class_rawexpr ->
-	  VernacCoercion (enforce_locality_exp (), AN qid, s, t)
+	  VernacCoercion (enforce_locality_exp true, AN qid, s, t)
       | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":";
 	 s = class_rawexpr; ">->"; t = class_rawexpr ->
-	  VernacCoercion (enforce_locality_exp (), ByNotation ntn, s, t)
+	  VernacCoercion (enforce_locality_exp true, ByNotation ntn, s, t)
       | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
 	  VernacCoercion (use_locality_exp (), AN qid, s, t)
@@ -799,10 +799,10 @@ GEXTEND Gram
 
   syntax:
    [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
-         VernacOpenCloseScope (enforce_locality_of local,true,sc)
+         VernacOpenCloseScope (enforce_section_locality local,true,sc)
 
      | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
-         VernacOpenCloseScope (enforce_locality_of local,false,sc)
+         VernacOpenCloseScope (enforce_section_locality local,false,sc)
 
      | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc,key)
@@ -812,22 +812,23 @@ GEXTEND Gram
 
      | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
        "["; scl = LIST0 opt_scope; "]" ->
-	 VernacArgumentsScope (use_section_non_locality (),qid,scl)
+	 VernacArgumentsScope (use_section_locality (),qid,scl)
 
      | IDENT "Infix"; local = obsolete_locality;
 	 op = ne_string; ":="; p = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         VernacInfix (enforce_locality_of local,(op,modl),p,sc)
+         VernacInfix (enforce_module_locality local,(op,modl),p,sc)
      | 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)
+           VernacSyntacticDefinition
+	     (id,(idl,c),enforce_module_locality local,b)
      | 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)
+           VernacNotation (enforce_module_locality local,c,(s,modl),sc)
 
      | IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
 	 pil = LIST1 production_item; ":="; t = Tactic.tactic
@@ -836,12 +837,12 @@ GEXTEND Gram
      | IDENT "Reserved"; IDENT "Infix"; s = ne_string;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
 	   Metasyntax.check_infix_modifiers l;
-	   VernacSyntaxExtension (use_locality (),("x '"^s^"' y",l))
+	   VernacSyntaxExtension (use_module_locality (),("x '"^s^"' y",l))
 
      | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
 	 s = ne_string;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (enforce_locality_of local,(s,l))
+	 -> VernacSyntaxExtension (enforce_module_locality local,(s,l))
 
      (* "Print" "Grammar" should be here but is in "command" entry in order
         to factorize with other "Print"-based vernac entries *)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 9f185c260c..76098e4fb1 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -155,6 +155,10 @@ let pr_locality_full = function
   | Some false -> str"Global "
 let pr_locality local = if local then str "Local " else str ""
 let pr_non_locality local = if local then str "" else str "Global "
+let pr_section_locality local =
+  if Lib.sections_are_opened () && not local then str "Global "
+  else if not (Lib.sections_are_opened ()) && local then str "Local "
+  else mt ()
 
 let pr_explanation (e,b,f) =
   let a = match e with
@@ -499,7 +503,8 @@ let rec pr_vernac = function
   (* Syntax *)
   | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e)
   | VernacOpenCloseScope (local,opening,sc) ->
-      str (if opening then "Open " else "Close ") ++ pr_locality local ++
+      pr_section_locality local ++ 
+      str (if opening then "Open " else "Close ") ++
       str "Scope" ++ spc() ++ str sc
   | VernacDelimiters (sc,key) ->
       str"Delimit Scope" ++ spc () ++ str sc ++
@@ -510,11 +515,11 @@ let rec pr_vernac = function
   | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function
       |	None -> str"_"
       |	Some sc -> str sc in
-    str"Arguments Scope" ++ spc() ++ pr_non_locality local ++
+    pr_section_locality local ++ str"Arguments Scope" ++ spc() ++ 
     pr_smart_global q
     ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
   | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *)
-      hov 0 (hov 0 (str"Infix " ++ pr_locality local
+      hov 0 (hov 0 (pr_locality local ++ str"Infix "
       ++ qs s ++ str " :=" ++ pr_constrarg q) ++
       pr_syntax_modifiers mv ++
       (match sn with
@@ -528,13 +533,13 @@ let rec pr_vernac = function
           let s' = String.sub s 1 (n-2) in
           if String.contains s' '\'' then qs s else str s'
 	else qs s in
-      hov 2 (str"Notation" ++ spc() ++ pr_locality local ++ ps ++
+      hov 2 (pr_locality local ++ str"Notation" ++ spc() ++ ps ++
       str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
       (match opt with
         | None -> mt()
         | Some sc -> str" :" ++ spc() ++ str sc))
   | VernacSyntaxExtension (local,(s,l)) ->
-      str"Reserved Notation" ++ spc() ++ pr_locality local ++ qs s ++
+      pr_locality local ++ str"Reserved Notation" ++ spc() ++ qs s ++
       pr_syntax_modifiers l
 
   (* Gallina *)
@@ -806,7 +811,7 @@ let rec pr_vernac = function
   | VernacChdir s -> str"Cd" ++ pr_opt qs s
 
   (* Commands *)
-  | VernacDeclareTacticDefinition (rc,l) ->
+  | VernacDeclareTacticDefinition (local,rc,l) ->
       let pr_tac_body (id, redef, body) =
         let idl, body =
           match body with
@@ -823,21 +828,22 @@ let rec pr_vernac = function
 	  (Global.env())
 	  body in
       hov 1
-        ((str "Ltac ") ++
+        (pr_locality local ++ str "Ltac " ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
   | VernacCreateHintDb (local,dbname,b) ->
-      hov 1 (str "Create " ++ pr_locality local ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ()))
+      hov 1 (pr_locality local ++ str "Create " ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ()))
   | VernacHints (local,dbnames,h) ->
       pr_hints local dbnames h pr_constr pr_constr_pattern_expr
   | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
       hov 2
-        (str"Notation " ++ pr_locality local ++ pr_lident id ++
+        (pr_locality local ++ str"Notation " ++ pr_lident id ++
 	 prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
   | VernacDeclareImplicits (local,q,None) ->
-      hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q)
+      hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ 
+	pr_smart_global q)
   | VernacDeclareImplicits (local,q,Some imps) ->
-      hov 1 (str"Implicit Arguments " ++ pr_non_locality local ++
+      hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++ 
 	spc() ++ pr_smart_global q ++ spc() ++
 	str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
   | VernacReserve (idl,c) ->
@@ -860,7 +866,7 @@ let rec pr_vernac = function
       let pr_line (l,q) =
         hov 2 (pr_lev l ++ spc() ++
                str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") in
-      hov 1 (pr_locality local ++ str"Strategy" ++ spc() ++
+      hov 1 (pr_non_locality local ++ str"Strategy" ++ spc() ++
              hv 0 (prlist_with_sep sep pr_line l))
   | VernacUnsetOption (l,na) ->
       hov 1 (pr_locality_full l ++ str"Unset" ++ spc() ++ pr_printoption na None)