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

fixing two opened bugs from HoTT/coq.

1 files changed, 1 insertions, 1 deletions

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