Add an e_type_of to avoid losing universe constraints.

1 files changed, 1 insertions, 0 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 0ff6b69a5c..dc88795216 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -123,6 +123,7 @@ let make_inv_predicate env evd indf realargs id status concl =
         let refl_term = eqdata.Coqlib.refl in
 	let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
         let refl = mkApp (refl_term, [|eqnty; rhs|]) in
+	let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd refl in
         let args = refl :: args in
         build_concl eqns args (succ n) restlist
   in