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

2 files changed, 44 insertions, 1 deletions

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.