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

fixing two opened bugs from HoTT/coq.

7 files changed, 19 insertions, 19 deletions

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 5cd05c58d6..2f34f7efea 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -285,11 +285,13 @@ let sort_of env evd c =
 
 (* Try to solve the existential variables by typing *)
 
-let e_type_of env evd c =
+let e_type_of ?(refresh=false) env evd c =
   let evdref = ref evd in
   let j = execute env evdref c in
   (* side-effect on evdref *)
-  !evdref, j.uj_type
+    if refresh then
+      Evarsolve.refresh_universes false !evdref j.uj_type
+    else !evdref, j.uj_type
 
 let solve_evars env evdref c =
   let c = (execute env evdref c).uj_val in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 8b194a9c9a..26dc8c560e 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -17,8 +17,9 @@ open Evd
 (** Typecheck a term and return its type *)
 val type_of : env -> evar_map -> constr -> types
 
-(** Typecheck a term and return its type + updated evars *)
-val e_type_of : env -> evar_map -> constr -> evar_map * types
+(** Typecheck a term and return its type + updated evars, optionally refreshing
+    universes *)
+val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 
 (** Typecheck a type and return its sort *)
 val sort_of : env -> evar_map -> types -> sorts
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0d2b3d5a1f..69505172cb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -650,7 +650,7 @@ let interp_may_eval f ist env sigma = function
 	    str "Unbound context identifier" ++ pr_id s ++ str"."))
   | ConstrTypeOf c ->
       let (sigma,c_interp) = f ist env sigma c in
-      sigma , Typing.type_of env sigma c_interp
+      Typing.e_type_of ~refresh:true env sigma c_interp
   | ConstrTerm c ->
      try
 	f ist env sigma c
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 0000000000..370c7d404e
--- /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 0000000000..341128338e
--- /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 7c88447b29..0000000000
--- 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 e293e6dbbb..0000000000
--- 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. *)