Refresh universes for Ltac's type_of, as the term can be used anywhere,

fixing two opened bugs from HoTT/coq.

4 files changed, 11 insertions, 14 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_074.v b/test-suite/bugs/closed/HoTT_coq_074.v
new file mode 100644
index 000000000..370c7d404
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_074.v
@@ -0,0 +1,10 @@
+Monomorphic Definition U1 := Type.
+Monomorphic Definition U2 := Type.
+
+Set Printing Universes.
+Definition foo : True.
+let t1 := type of U1 in
+let t2 := type of U2 in
+idtac t1 t2;
+pose (t1 : t2). exact I. 
+Defined.
diff --git a/test-suite/bugs/closed/HoTT_coq_114.v b/test-suite/bugs/closed/HoTT_coq_114.v
new file mode 100644
index 000000000..341128338
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_114.v
@@ -0,0 +1 @@
+Inductive test : $(let U := type of Type in exact U)$ := t.
diff --git a/test-suite/bugs/opened/HoTT_coq_074.v b/test-suite/bugs/opened/HoTT_coq_074.v
deleted file mode 100644
index 7c88447b2..000000000
--- a/test-suite/bugs/opened/HoTT_coq_074.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Monomorphic Definition U1 := Type.
-Monomorphic Definition U2 := Type.
-
-Set Printing Universes.
-Definition foo : True.
-Fail let t1 := type of U1 in
-let t2 := type of U2 in
-pose (t1 : t2). (* Error:
-The term "Type (* Top.1+1 *)" has type "Type (* Top.1+2 *)"
-while it is expected to have type "Type (* Top.2+1 *)". *)
-exact I.
-Defined.
diff --git a/test-suite/bugs/opened/HoTT_coq_114.v b/test-suite/bugs/opened/HoTT_coq_114.v
deleted file mode 100644
index e293e6dbb..000000000
--- a/test-suite/bugs/opened/HoTT_coq_114.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Fail Inductive test : $(let U := type of Type in exact U)$ := t.
-(* Anomaly: Unable to handle arbitrary u+k <= v constraints. Please report. *)