From d6ff0fcefa21bd2c6424627049b0f5e49ed4df12 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 8 Oct 2015 14:58:11 +0200
Subject: Univs: fix bug #4161.

Retypecheck abstracted infered predicate to register the right
universe constraints.
---
 test-suite/bugs/closed/4161.v | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 test-suite/bugs/closed/4161.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4161.v b/test-suite/bugs/closed/4161.v
new file mode 100644
index 0000000000..aa2b189b67
--- /dev/null
+++ b/test-suite/bugs/closed/4161.v
@@ -0,0 +1,27 @@
+
+    (* Inductive t : Type -> Type := *)
+    (* | Just : forall (A : Type), t A -> t A. *)
+
+    (* Fixpoint test {A : Type} (x : t A) : t (A + unit) := *)
+    (*   match x in t A return t (A + unit) with *)
+    (*   | Just T x => @test T x *)
+    (*   end. *)
+
+
+    Definition Type1 := Type.
+Definition Type2 := Type.
+Definition cast (x:Type2) := x:Type1.
+Axiom f: Type2 -> Prop.
+Definition A :=
+ let T := fun A:Type1 => _ in
+ fun A':Type2 =>
+ eq_refl : T A' = f A' :> Prop.
+(* Type2 <= Type1... f A -> Type1 <= Type2 *)
+
+Inductive t : Type -> Type :=
+    | Just : forall (A : Type), t A -> t A.
+
+Fixpoint test {A : Type} (x : t A) : t (A + unit) :=
+  match x in t A with
+  | Just B x => @test B x
+  end.
\ No newline at end of file
-- 
cgit v1.2.3