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

1 files changed, 11 insertions, 3 deletions

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 =