1 files changed, 32 insertions, 4 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 1adcbd39..203fbbb7 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -1,4 +1,32 @@
-(* Check local definitions in context of inductive types *)
+(* Test des definitions inductives imbriquees *)
+
+Require Import List.
+
+Inductive X : Set :=
+    cons1 : list X -> X.
+
+Inductive Y : Set :=
+    cons2 : list (Y * Y) -> Y.
+
+(* Test inductive types with local definitions (arity) *)
+
+Inductive eq1 : forall A:Type, let B:=A in A -> Prop :=
+  refl1 : eq1 True I.
+
+Check
+ fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) =>
+   let B := A in
+     fun (a : A) (e : eq1 A a) =>
+       match e in (eq1 A0 B0 a0) return (P A0 a0) with
+       | refl1 => f
+       end.
+
+Inductive eq2 (A:Type) (a:A)
+  : forall B C:Type, let D:=(A*B*C)%type in D -> Prop :=
+  refl2 : eq2 A a unit bool (a,tt,true).
+
+(* Check inductive types with local definitions (parameters) *)
+
 Inductive A (C D : Prop) (E:=C) (F:=D) (x y : E -> F) : E -> Set :=
     I : forall z : E, A C D x y z.
 
@@ -7,9 +35,9 @@ Check
    let E := C in
    let F := D in
    fun (x y : E -> F) (P : forall c : C, A C D x y c -> Type)
-     (f : forall z : C, P z (I C D x y z)) (y0 : C) 
+     (f : forall z : C, P z (I C D x y z)) (y0 : C)
      (a : A C D x y y0) =>
-   match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with
+   match a as a0 in (A _ _ _ _ _ _ y1) return (P y1 a0) with
    | I x0 => f x0
    end).
 
@@ -20,7 +48,7 @@ Check
    let E := C in
    let F := D in
    fun (x y : E -> F) (P : B C D x y -> Type)
-     (f : forall p0 q0 : C, P (Build_B C D x y p0 q0)) 
+     (f : forall p0 q0 : C, P (Build_B C D x y p0 q0))
      (b : B C D x y) =>
    match b as b0 return (P b0) with
    | Build_B x0 x1 => f x0 x1