1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index ce9050d421..8c8f02eccf 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -17,3 +17,27 @@ Definition foo (x : I') : bool :=
   match x with
   C' => true
   end.
+
+(* Bug found in november 2015: was wrongly failing in 8.5beta2 and 8.5beta3 *)
+
+Inductive I2 (A:Type) : let B:=A in forall C, let D:=(C*B)%type in Type :=
+  E2 : I2 A nat.
+
+Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with
+  E2 _ => (0,0,(0,0))
+  end.
+
+(* This used to succeed in 8.3, 8.4 and 8.5beta1 *)
+
+Inductive IND : forall X:Type, let Y:=X in Type :=
+  C : IND True.
+
+Definition F (x:IND True) (A:Type) :=
+  (* This failed in 8.5beta2 though it should have been accepted *)
+  match x in IND Y Z return Z with
+  C => I
+  end.
+
+Theorem paradox : False.
+  (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
+Fail Proof (F C False).