From 8b90dc406730123640f186c8b39f6329a3f434a4 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 20 Jun 2014 12:16:20 +0200
Subject: Add an e_type_of to avoid losing universe constraints.

---
 tactics/inv.ml | 1 +
 1 file changed, 1 insertion(+)

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
-- 
cgit v1.2.3