1 files changed, 18 insertions, 4 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index da5dd5e4..3d425754 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -17,7 +17,7 @@ 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
+       match e in (@eq1 A0 B0 a0) return (P A0 a0) with
        | refl1 => f
        end.
 
@@ -37,8 +37,8 @@ Check
    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)
      (a : A C D x y y0) =>
-   match a as a0 in (A _ _ _ _ _ _ y1) return (P y1 a0) with
-   | I x0 => f x0
+   match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with
+   | I _ _ _ _ x0 => f x0
    end).
 
 Record B (C D : Set) (E:=C) (F:=D) (x y : E -> F) : Set :=  {p : C; q : E}.
@@ -51,7 +51,7 @@ Check
      (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
+   | Build_B _ _ _ _ x0 x1 => f x0 x1
    end).
 
 (* Check inductive types with local definitions (constructors) *)
@@ -107,3 +107,17 @@ Set Implicit Arguments.
 Inductive I A : A->Prop := C a : (forall A, A) -> I a.
 
  *)
+
+(* Test recursively non-uniform parameters (was formerly in params_ind.v) *)
+
+Inductive list (A : Set) : Set :=
+  | nil : list A
+  | cons : A -> list (A -> A) -> list A.
+
+(* Check inference of evars in arity using information from constructors *)
+
+Inductive foo1 : forall p, Prop := cc1 : foo1 0.
+
+(* Check cross inference of evars from constructors *)
+
+Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0.