From 4849c8eb1b7a386d2abcbc80c40de34b0a69b8ea Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 16 Mar 2016 18:18:54 +0100
Subject: Test file for #4624, fixed by Matthieu's bfce815bd1.

---
 test-suite/bugs/4624.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/4624.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/4624.v
new file mode 100644
index 0000000000..a737afcdab
--- /dev/null
+++ b/test-suite/bugs/4624.v
@@ -0,0 +1,7 @@
+Record foo := mkfoo { type : Type }.
+
+Canonical Structure fooA (T : Type) := mkfoo (T -> T).
+
+Definition id (t : foo) (x : type t) := x.
+
+Definition bar := id _ ((fun x : nat => x) : _).
\ No newline at end of file
-- 
cgit v1.2.3


From bcee0b4d6ca113d225fa7df1cbcfa33812b0bd46 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 17 Mar 2016 18:06:50 +0100
Subject: Test file for #4623.

---
 test-suite/bugs/4623.v | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 test-suite/bugs/4623.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/4623.v
new file mode 100644
index 0000000000..405d09809c
--- /dev/null
+++ b/test-suite/bugs/4623.v
@@ -0,0 +1,5 @@
+Goal Type -> Type.
+set (T := Type).
+clearbody T.
+refine (@id _).
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3


From c8dcfc691a649ff6dfb3416809c6ec7b1e629b1f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 17 Mar 2016 20:23:00 +0100
Subject: Fix bug #4627: records with no declared arity can be template
 polymorphic.

As if we were adding : Type. Consistent with inductives with no
declared arity.
---
 test-suite/bugs/closed/4627.v | 49 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 test-suite/bugs/closed/4627.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4627.v b/test-suite/bugs/closed/4627.v
new file mode 100644
index 0000000000..e1206bb37a
--- /dev/null
+++ b/test-suite/bugs/closed/4627.v
@@ -0,0 +1,49 @@
+Class sa (A:Type) := { }.
+
+Record predicate A (sa:sa A) :=
+  { pred_fun: A->Prop }.
+Record ABC : Type :=
+  { abc: Type }.
+Record T :=
+  { T_abc: ABC }.
+
+
+(*
+sa: forall _ : Type@{Top.179}, Prop
+predicate: forall (A : Type@{Top.205}) (_ : sa A), Type@{max(Set+1, Top.205)}
+T: Type@{Top.208+1}
+ABC: Type@{Top.208+1}
+abc: forall _ : ABC, Type@{Top.208}
+
+Top.205 <= Top.179   predicate <= sa.A
+Set < Top.208        Set < abc
+Set < Top.205        Set < predicate
+*)
+
+Definition foo : predicate T (Build_sa T) :=
+    {| pred_fun:= fun w => True |}.
+(* *)
+(* Top.208 < Top.205   <--- added by foo *)
+(* *)
+
+Check predicate nat (Build_sa nat).
+(*
+
+The issue is that the template polymorphic universe of [predicate], Top.205, does not get replaced with the universe of [nat] in the above line.
+  -Jason Gross
+
+8.5          -- predicate nat (Build_sa nat): Type@{max(Set+1, Top.205)}
+8.5 EXPECTED -- predicate nat (Build_sa nat): Type@{Set+1}
+8.4pl4       -- predicate nat {| |}: Type (* max(Set, (Set)+1) *)
+*)
+
+(* This works in 8.4pl4 and SHOULD work in 8.5 *)
+Definition bar : ABC :=
+  {| abc:= predicate nat (Build_sa nat) |}.
+(*
+The term "predicate nat (Build_sa nat)" has type
+ "Type@{max(Set+1, Top.205)}"
+while it is expected to have type "Type@{Top.208}"
+(universe inconsistency: Cannot enforce Top.205 <=
+Top.208 because Top.208 < Top.205).
+*)
\ No newline at end of file
-- 
cgit v1.2.3