Local/Global revision 12418 continued

- Fixing non-export of newly created Local Argument Scope.
- Fixing bad discharge of local variables in nested sections
  (bug still exists in v8.2).

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

4 files changed, 53 insertions, 11 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 093d43934..6ae720fca 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -482,18 +482,16 @@ 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
@@ -504,7 +502,7 @@ 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 is_local local ref = local || isVarRef ref && Lib.is_in_section ref
 
 let declare_arguments_scope_gen req r scl =
   Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl))
diff --git a/library/impargs.ml b/library/impargs.ml
index 89f34a38b..c434be70d 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -473,7 +473,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) ->
       let vars = section_segment_of_reference ref in
-      let ref' = pop_global_reference ref in
+      let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let l' = [ref', impls_of_context vars @ snd (List.hd l)] in
       Some (ImplInteractive (ref',flags,exp),l')
   | ImplConstant (con,flags) ->
@@ -483,7 +483,8 @@ let discharge_implicits (_,(req,l)) =
   | ImplMutualInductive (kn,flags) ->
       let l' = List.map (fun (gr, l) ->
 	let vars = section_segment_of_reference gr in
-	  (pop_global_reference gr, impls_of_context vars @ l)) l
+	((if isVarRef gr then gr else pop_global_reference gr),
+	 impls_of_context vars @ l)) l
       in
 	Some (ImplMutualInductive (pop_kn kn,flags),l')
 
@@ -523,18 +524,18 @@ let rebuild_implicits (req,l) =
 	  [ref,l']
 
 let classify_implicits (req,_ as obj) =
-  if req = ImplLocal then None else Some obj
+  if req = ImplLocal then Dispose else Substitute obj
 
 let (inImplicits, _) =
   declare_object {(default_object "IMPLICITS") with
     cache_function = cache_implicits;
     load_function = load_implicits;
     subst_function = subst_implicits;
-    classify_function = (fun x -> Substitute x);
+    classify_function = classify_implicits;
     discharge_function = discharge_implicits;
     rebuild_function = rebuild_implicits }
 
-let is_local local ref = local || (isVarRef ref && not (is_in_section ref))
+let is_local local ref = local || isVarRef ref && is_in_section ref
 
 let declare_implicits_gen req flags ref =
   let imps = compute_global_implicits flags [] ref in
diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v
index cdb7a2691..8700a6c4e 100644
--- a/test-suite/prerequisite/make_local.v
+++ b/test-suite/prerequisite/make_local.v
@@ -5,6 +5,6 @@ Definition f (A:Type) (a:A) := a.
 Local Arguments Scope f [type_scope type_scope].
 Local Implicit Arguments f [A].
 
-(* Used in Import.v to test the locality flag *)
+(* Used in ImportedCoercion.v to test the locality flag *)
 
 Local Coercion g (b:bool) := if b then 0 else 1.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index aabb057a4..c6d0a6dd2 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -1,3 +1,5 @@
+(* Testing the behavior of implicit arguments *)
+
 (* Implicit on section variables *)
 
 Set Implicit Arguments.
@@ -19,8 +21,49 @@ Check
   (forall (type : Set) (elt : type) (empty : type -> bool),
    empty elt = true -> stack).
 
+(* Nested sections and manual implicit arguments *)
+
+Variable op' : forall A : Set, A -> A -> Set.
+Variable op'' : forall A : Set, A -> A -> Set.
+
+Section B.
+
+Definition eq1 := fun (A:Type) (x y:A) => x=y.
+Definition eq2 := fun (A:Type) (x y:A) => x=y.
+Definition eq3 := fun (A:Type) (x y:A) => x=y.
+
+Implicit Arguments op' [].
+Global Implicit Arguments op'' [].
+
+Implicit Arguments eq2 [].
+Global Implicit Arguments eq3 [].
+
+Check (op 0 0).
+Check (op' nat 0 0).
+Check (op'' nat 0 0).
+Check (eq1 0 0).
+Check (eq2 nat 0 0).
+Check (eq3 nat 0 0).
+
+End B.
+
+Check (op 0 0).
+Check (op' 0 0).
+Check (op'' nat 0 0).
+Check (eq1 0 0).
+Check (eq2 0 0).
+Check (eq3 nat 0 0).
+
 End Spec.
 
+Check (eq1 0 0).
+Check (eq2 0 0).
+Check (eq3 nat 0 0).
+
+(* Test discharge on automatic implicit arguments *)
+
+Check (op' 0 0).
+
 (* Example submitted by Frédéric (interesting in v8 syntax) *)
 
 Parameter f : nat -> nat * nat.