1 files changed, 42 insertions, 2 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 9034d6a6..59e1a935 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.
@@ -12,15 +14,53 @@ Infix "#" := op (at level 70).
 Check (forall x : A, x # x).
 
 (* Example submitted by Christine *)
-Record stack : Type := 
+
+Record stack : Type :=
   {type : Set; elt : type; empty : type -> bool; proof : empty elt = true}.
 
 Check
   (forall (type : Set) (elt : type) (empty : type -> bool),
    empty elt = true -> stack).
 
+(* Nested sections and manual/automatic 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).
+
 (* Example submitted by Frédéric (interesting in v8 syntax) *)
 
 Parameter f : nat -> nat * nat.
@@ -42,7 +82,7 @@ Inductive P n : nat -> Prop := c : P n n.
 Require Import List.
 
 Fixpoint plus n m {struct n} :=
-  match n with 
+  match n with
   | 0 => m
   | S p => S (plus p m)
   end.