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

17 files changed, 190 insertions, 118 deletions

diff --git a/CHANGES b/CHANGES
index 563ab83ad..681bd791d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -56,6 +56,8 @@ Vernacular commands
   referring to the constant by a notation string.
 - Added "Reserved Infix" as a specific shortcut of the corresponding
   "Reserved Notation".
+- Open/Close Scope command supports Global option in sections.
+- Ltac definitions support Local option for non-export outside modules.
 
 Tools
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 3948bbe85..8be2e0b06 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -186,7 +186,7 @@ is understood as
 \begin{figure}[ht]
 \begin{centerframe}
 \begin{tabular}{lcl}
-\nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
+\nterm{top} & ::= & \zeroone{\tt Local} {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
 \\
 \nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=}
 {\tacexpr}\\
@@ -864,6 +864,9 @@ A previous definition of \qualid must exist in the environment.
 The new definition will always be used instead of the old one and
 it goes accross module boundaries.
 
+If preceded by the keyword {\tt Local} the tactic definition will not
+be exported outside the current module.
+
 \subsection[Printing {\ltac} tactics]{Printing {\ltac} tactics\comindex{Print Ltac}}
 
 Defined {\ltac} functions can be displayed using the command
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index a5678eacf..d37fc9f3f 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -700,6 +700,13 @@ exported to the modules that import the module where they occur.
 These variants are not exported to the modules that import the module
 where they occur, even if outside a section.
 
+\item {\tt Global Open Scope} {\scope}.
+
+\item {\tt Global Close Scope} {\scope}.
+
+These variants survive sections. They behave as if {\tt Global} were
+absent when not inside a section.
+
 \end{Variants}
 
 \subsection{Local interpretation rules for notations}
diff --git a/interp/notation.ml b/interp/notation.ml
index e3eb38af6..093d43934 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -113,6 +113,9 @@ let subst_scope (subst,sc) = sc
 
 open Libobject
 
+let discharge_scope (local,_,_ as o) =
+  if local then None else Some o
+
 let classify_scope (local,_,_ as o) =
   if local then Dispose else Substitute o
 
@@ -479,16 +482,18 @@ let classify_arguments_scope (req,_,_ as obj) =
   if req = ArgsScopeNoDischarge then Dispose else Substitute obj
 
 let rebuild_arguments_scope (req,r,l) =
+  let req' =
+    if isVarRef r && Lib.is_in_section r then ArgsScopeNoDischarge else req in
   match req with
     | ArgsScopeNoDischarge -> assert false
     | ArgsScopeAuto ->
-	(req,r,compute_arguments_scope (Global.type_of_global r))
+	(req',r,compute_arguments_scope (Global.type_of_global r))
     | ArgsScopeManual ->
 	(* Add to the manually given scopes the one found automatically
            for the extra parameters of the section *)
 	let l' = compute_arguments_scope (Global.type_of_global r) in
 	let l1,_ = list_chop (List.length l' - List.length l) l' in
-	(req,r,l1@l)
+	(req',r,l1@l)
 
 let (inArgumentsScope,outArgumentsScope) =
   declare_object {(default_object "ARGUMENTS-SCOPE") with
@@ -499,11 +504,14 @@ let (inArgumentsScope,outArgumentsScope) =
       discharge_function = discharge_arguments_scope;
       rebuild_function = rebuild_arguments_scope }
 
+let is_local local ref = local || (isVarRef ref && not (Lib.is_in_section ref))
+
 let declare_arguments_scope_gen req r scl =
   Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl))
 
 let declare_arguments_scope local ref scl =
-  let req = if local then ArgsScopeNoDischarge else ArgsScopeManual in
+  let req =
+    if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in
   declare_arguments_scope_gen req ref scl
 
 let find_arguments_scope r =
diff --git a/library/impargs.ml b/library/impargs.ml
index dec961793..89f34a38b 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -488,12 +488,12 @@ let discharge_implicits (_,(req,l)) =
 	Some (ImplMutualInductive (pop_kn kn,flags),l')
 
 let rebuild_implicits (req,l) =
-  let l' = match req with
+  match req with
   | ImplLocal -> assert false
   | ImplConstant (con,flags) ->
       let oldimpls = snd (List.hd l) in
       let newimpls = compute_constant_implicits flags [] con in
-      [ConstRef con, merge_impls oldimpls newimpls]
+      req, [ConstRef con, merge_impls oldimpls newimpls]
   | ImplMutualInductive (kn,flags) ->
       let newimpls = compute_all_mib_implicits flags [] kn in
       let rec aux olds news =
@@ -502,9 +502,10 @@ let rebuild_implicits (req,l) =
 	    (gr, merge_impls oldimpls newimpls) :: aux old tl
 	| [], [] -> []
 	| _, _ -> assert false
-      in aux l newimpls
+      in req, aux l newimpls
 
   | ImplInteractive (ref,flags,o) ->
+      (if isVarRef ref && is_in_section ref then ImplLocal else req),
       match o with
       | ImplAuto ->
 	  let oldimpls = snd (List.hd l) in
@@ -518,8 +519,8 @@ let rebuild_implicits (req,l) =
 		merge_impls oldimpls newimpls
 	    else oldimpls
 	  in
-	  let l' = merge_impls auto m in [ref,l']
-  in (req,l')
+	  let l' = merge_impls auto m in
+	  [ref,l']
 
 let classify_implicits (req,_ as obj) =
   if req = ImplLocal then None else Some obj
@@ -533,6 +534,8 @@ let (inImplicits, _) =
     discharge_function = discharge_implicits;
     rebuild_function = rebuild_implicits }
 
+let is_local local ref = local || (isVarRef ref && not (is_in_section ref))
+
 let declare_implicits_gen req flags ref =
   let imps = compute_global_implicits flags [] ref in
   add_anonymous_leaf (inImplicits (req,[ref,imps]))
@@ -540,7 +543,7 @@ let declare_implicits_gen req flags ref =
 let declare_implicits local ref =
   let flags = { !implicit_args with auto = true } in
   let req =
-    if local then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in
+    if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in
     declare_implicits_gen req flags ref
 
 let declare_var_implicits id =
@@ -572,7 +575,7 @@ let declare_manual_implicits local ref ?enriching l =
   let enriching = Option.default flags.auto enriching in
   let l' = compute_manual_implicits env flags t enriching l in
   let req =
-    if local or isVarRef ref then ImplLocal
+    if is_local local ref then ImplLocal
     else ImplInteractive(ref,flags,ImplManual l')
   in
     add_anonymous_leaf (inImplicits (req,[ref,l']))
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 7f63428c8..0e97b2a7f 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 90245fa45..39e577b88 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 28a66182c..e1a71ff23 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 9f185c260..76098e4fb 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)
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index d294af68d..b4e0e69bb 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1632,7 +1632,7 @@ let rec xlate_module_expr = function
 
 let rec xlate_vernac =
  function
-   | VernacDeclareTacticDefinition (true, tacs) ->
+   | VernacDeclareTacticDefinition (false, true, tacs) ->
        (match List.map
 	 (function
 	      (id, _, body) ->
@@ -1642,8 +1642,10 @@ let rec xlate_vernac =
 	   | fst::tacs1 ->
 	       CT_tactic_definition
 		 (CT_tac_def_ne_list(fst, tacs1)))
-   | VernacDeclareTacticDefinition(false, _) ->
-       xlate_error "obsolete tactic definition not handled"
+    | VernacDeclareTacticDefinition(_, false, _) ->
+	xlate_error "obsolete tactic definition not handled"
+    | VernacDeclareTacticDefinition(true, _, _) ->
+	xlate_error "TODO: Local keyword"
     | VernacLoad (verbose,s) ->
       CT_load (
        (match verbose with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 10d2a026e..bd0e9c7b4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2809,7 +2809,7 @@ let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab)
 type tacdef_kind = | NewTac of identifier
 		   | UpdateTac of ltac_constant
 
-let load_md i ((sp,kn),defs) =
+let load_md i ((sp,kn),(local,defs)) =
   let dp,_ = repr_path sp in
   let mp,dir,_ = repr_kn kn in
   List.iter (fun (id,t) ->
@@ -2821,7 +2821,7 @@ let load_md i ((sp,kn),defs) =
 	    add (kn,t)
       | UpdateTac kn -> replace (kn,t)) defs
 
-let open_md i((sp,kn),defs) =
+let open_md i ((sp,kn),(local,defs)) =
   let dp,_ = repr_path sp in
   let mp,dir,_ = repr_kn kn in
   List.iter (fun (id,t) ->
@@ -2839,8 +2839,12 @@ let subst_kind subst id =
     | NewTac _ -> id
     | UpdateTac kn -> UpdateTac (subst_kn subst kn)
 
-let subst_md (subst,defs) =
-  List.map (fun (id,t) -> (subst_kind subst id,subst_tactic subst t)) defs
+let subst_md (subst,(local,defs)) =
+  (local,
+   List.map (fun (id,t) -> (subst_kind subst id,subst_tactic subst t)) defs)
+
+let classify_md (local,defs as o) =
+  if local then Dispose else Substitute o
 
 let (inMD,outMD) =
   declare_object {(default_object "TAC-DEFINITION") with
@@ -2848,7 +2852,7 @@ let (inMD,outMD) =
      load_function   = load_md;
      open_function   = open_md;
      subst_function = subst_md;
-     classify_function = (fun o -> Substitute o)}
+     classify_function = classify_md}
 
 let print_ltac id =
  try
@@ -2885,7 +2889,7 @@ let make_absolute_name ident repl =
     user_err_loc (loc,"Tacinterp.add_tacdef",
 		 str "There is no Ltac named " ++ pr_reference ident ++ str".")
 
-let add_tacdef isrec tacl =
+let add_tacdef local isrec tacl =
   let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
   let ist =
     {(make_empty_glob_sign()) with ltacrecvars =
@@ -2899,8 +2903,9 @@ let add_tacdef isrec tacl =
 	(k, t))
       tacl rfun in
   let id0 = fst (List.hd rfun) in
-  let _ = match id0 with Some id0 -> ignore(Lib.add_leaf id0 (inMD gtacl))
-    | _ -> Lib.add_anonymous_leaf (inMD gtacl) in
+  let _ = match id0 with
+    | Some id0 -> ignore(Lib.add_leaf id0 (inMD (local,gtacl)))
+    | _ -> Lib.add_anonymous_leaf (inMD (local,gtacl)) in
   List.iter
     (fun (id,b,_) ->
       Flags.if_verbose msgnl (Libnames.pr_reference id ++
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 18873d1c6..238a329fd 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -67,7 +67,8 @@ val get_debug : unit -> debug_info
 
 (* Adds a definition for tactics in the table *)
 val add_tacdef :
-  bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit
+  Vernacexpr.locality_flag -> bool ->
+  (Libnames.reference * bool * raw_tactic_expr) list -> unit
 val add_primitive_tactic : string -> glob_tactic_expr -> unit
 
 (* Tactic extensions *)
diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
index ad1beb553..7abb68eea 100644
--- a/toplevel/protectedtoplevel.ml
+++ b/toplevel/protectedtoplevel.ml
@@ -132,7 +132,7 @@ let rec parse_one_command_group input_channel =
 		       | Some(rank, e) ->
 			   (match e with
                     	     | DuringCommandInterp(a,e1)
-			     | Stdpp.Exc_located (a,DuringSyntaxChecking e1) ->
+			     | DuringSyntaxChecking(a,e1) ->
 				  output_results_nl
 				    (acknowledge_command
 				       !global_request_id rank (Some e1))
@@ -167,7 +167,7 @@ let protected_loop input_chan =
       | DuringCommandInterp(loc, Vernacexpr.Quit) -> raise Vernacexpr.Quit
       | DuringCommandInterp(loc, Vernacexpr.Drop) -> raise Vernacexpr.Drop
       | DuringCommandInterp(loc, e)
-      | Stdpp.Exc_located (loc,DuringSyntaxChecking e) ->
+      | DuringSyntaxChecking(loc, e) ->
 	  explain_and_restart e
       | e -> explain_and_restart e in
     begin
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index d14acaab9..b57b9c1eb 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -275,7 +275,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
+  | DuringSyntaxChecking (_,e) -> is_pervasive_exn e
   | _ -> false
 
 (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
@@ -285,7 +285,7 @@ let print_toplevel_error exc =
   let (dloc,exc) =
     match exc with
       | DuringCommandInterp (loc,ie)
-      | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) ->
+      | DuringSyntaxChecking (loc,ie) ->
           if loc = dummy_loc then (None,ie) else (Some loc, ie)
       | _ -> (None, exc)
   in
@@ -337,7 +337,7 @@ let rec discard_to_dot () =
 
 let process_error = function
   | DuringCommandInterp _
-  | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e
+  | DuringSyntaxChecking _ as e -> e
   | e ->
       if is_pervasive_exn e then
 	e
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a14e8ad45..6d4ecf774 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -33,7 +33,7 @@ let raise_with_file file exc =
   let (cmdloc,re) =
     match exc with
       | DuringCommandInterp(loc,e)
-      | Stdpp.Exc_located (loc,DuringSyntaxChecking e) -> (loc,e)
+      | DuringSyntaxChecking(loc,e) -> (loc,e)
       | e -> (dummy_loc,e)
   in
   let (inner,inex) =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 664b05f1d..754f58a9c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -747,7 +747,8 @@ let vernac_backto n = Lib.reset_label n
 (************)
 (* Commands *)
 
-let vernac_declare_tactic_definition = Tacinterp.add_tacdef
+let vernac_declare_tactic_definition (local,x,def) =
+  Tacinterp.add_tacdef local x def
 
 let vernac_create_hintdb local id b =
   Auto.create_hint_db local id full_transparent_state b
@@ -1368,7 +1369,7 @@ let interp c = match c with
   | VernacBackTo n -> vernac_backto n
 
   (* Commands *)
-  | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
+  | VernacDeclareTacticDefinition def -> vernac_declare_tactic_definition def
   | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 96960540b..cedd20e08 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -293,7 +293,7 @@ type vernac_expr =
 
   (* Commands *)
   | VernacDeclareTacticDefinition of
-      rec_flag * (reference * bool * raw_tactic_expr) list
+      (locality_flag * rec_flag * (reference * bool * raw_tactic_expr) list)
   | VernacCreateHintDb of locality_flag * lstring * bool
   | VernacHints of locality_flag * lstring list * hints_expr
   | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
@@ -344,65 +344,41 @@ 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
+exception DuringSyntaxChecking of exn located
 
-let syntax_checking_error s =
-  raise (DuringSyntaxChecking (UserError ("",Pp.str s)))
+let syntax_checking_error loc s =
+  raise (DuringSyntaxChecking (loc,UserError ("",Pp.str s)))
 
+(**********************************************************************)
 (* Managing locality *)
 
 let locality_flag = ref None
 
 let local_of_bool = function true -> Local | false -> Global
 
-let check_locality () =
-  if !locality_flag = Some true then
-    syntax_checking_error "This command does not support the \"Local\" prefix.";
-  if !locality_flag = Some false then
-    syntax_checking_error "This command does not support the \"Global\" prefix."
-
-let use_locality_full () =
-  let r = !locality_flag in
-  locality_flag := None;
-   r
-
-let use_locality () =
-  match use_locality_full () with Some true -> true | _ -> false
-
-let use_locality_exp () = local_of_bool (use_locality ())
-
-let use_section_locality () =
-  match use_locality_full () with Some b -> b | None -> Lib.sections_are_opened ()
-
-let use_non_locality () =
-  match use_locality_full () with Some false -> false | _ -> true
-
-let use_section_non_locality () =
-  match use_locality_full () with Some b -> b | None -> Lib.sections_are_opened ()
+let is_true = function Some (_,b) -> b | _ -> false
+let is_false = function Some (_,b) -> not b | _ -> false
 
-let enforce_locality () =
-  let local =
-    match !locality_flag with
-    | Some false ->
-	error "Cannot be simultaneously Local and Global."
-    | _ ->
-	Flags.if_verbose
-	  Pp.warning "Obsolete syntax: use \"Local\" as a prefix.";
-	true in
-  locality_flag := None;
-  local
+let check_locality () =
+  match !locality_flag with
+  | Some (loc,true) -> 
+      syntax_checking_error loc
+	"This command does not support the \"Local\" prefix.";
+  | Some (loc,false) -> 
+      syntax_checking_error loc
+	"This command does not support the \"Global\" prefix."
+  | None -> ()
 
-(* [enforce_locality_exp] supports Local (with effect in section) but not
-   Global in section *)
+(** Extracting the locality flag *)
 
-let enforce_locality_exp () = local_of_bool (enforce_locality ())
+(* Commands which supported an inlined Local flag *)
 
-let enforce_full_locality_of local =
+let enforce_locality_full local =
   let local =
     match !locality_flag with
-    | Some false when local ->
+    | Some (_,false) when local ->
 	error "Cannot be simultaneously Local and Global."
-    | Some true when local ->
+    | Some (_,true) when local ->
 	error "Use only prefix \"Local\"."
     | None ->
 	if local then begin
@@ -411,18 +387,75 @@ let enforce_full_locality_of local =
 	  Some true
 	end else
 	None
-    | Some _ as b -> b in
+    | Some (_,b) -> Some b in
   locality_flag := None;
   local
 
-(* [enforce_locality_of] supports Local (with effect if not in
-   section) but not Global in section *)
-
-let enforce_locality_of local =
-  match enforce_full_locality_of local with
-    | Some false ->
-	if Lib.sections_are_opened () then
-	  error "This command does not support the Global option in sections.";
-	false
-    | Some true -> true 
-    | None -> false
+(* Commands which did not supported an inlined Local flag (synonym of
+   [enforce_locality_full false]) *)
+
+let use_locality_full () =
+  let r = Option.map snd !locality_flag in
+  locality_flag := None;
+   r
+
+(** Positioning locality for commands supporting discharging and export
+     outside of modules *)
+
+(* For commands whose default is to discharge and export:
+   Global is the default and is neutral;
+   Local in a section deactivate discharge, 
+   Local not in a section deactivates export *)
+
+let make_locality = function Some true -> true | _ -> false
+
+let use_locality () = make_locality (use_locality_full ())
+
+let use_locality_exp () = local_of_bool (use_locality ())
+
+let enforce_locality local = make_locality (enforce_locality_full local)
+
+let enforce_locality_exp local = local_of_bool (enforce_locality local)
+
+(* For commands whose default is not to discharge and not to export:
+   Global forces discharge and export;
+   Local is the default and is neutral *)
+
+let use_non_locality () =
+  match use_locality_full () with Some false -> false | _ -> true
+
+(* For commands whose default is to not discharge but to export:
+   Global in sections forces discharge, Global not in section is the default;
+   Local in sections is the default, Local not in section forces non-export *)
+
+let make_section_locality =
+  function Some b -> b | None -> Lib.sections_are_opened ()
+
+let use_section_locality () =
+  make_section_locality (use_locality_full ())
+
+let enforce_section_locality local =
+  make_section_locality (enforce_locality_full local)
+
+(** Positioning locality for commands supporting export but not discharge *)
+
+(* For commands whose default is to export (if not in section):
+   Global in sections is forbidden, Global not in section is neutral;
+   Local in sections is the default, Local not in section forces non-export *)
+
+let make_module_locality = function
+  | Some false ->
+      if Lib.sections_are_opened () then
+	error "This command does not support the Global option in sections.";
+      false
+  | Some true -> true
+  | None -> false
+
+let use_module_locality () =
+  make_module_locality (use_locality_full ())
+
+let enforce_module_locality local =
+  make_module_locality (enforce_locality_full local)
+
+(**********************************************************************)
+