Be more conservative and keep the use of eq_constr in pretyping/ functions.

1 files changed, 16 insertions, 5 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index bd105c7287..e49ed7b453 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1333,24 +1333,35 @@ let test_conversion env d pb t u =
   try conversion_gen env d pb t u; true
   with _ -> false
 
-let eq_constr d t u =
-  Term.eq_constr_univs d.universes.uctx_universes t u
+let eq_constr evd t u =
+  let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
+    if b then 
+      try let evd' = add_universe_constraints evd c in evd', b
+      with Univ.UniverseInconsistency _ -> evd, false
+    else evd, b
+
+let e_eq_constr evdref t u =
+  let evd, b = eq_constr !evdref t u in
+    evdref := evd; b
+
+let eq_constr_test evd t u =
+  snd (eq_constr evd t u)
 
 let eq_named_context_val d ctx1 ctx2 = 
   ctx1 == ctx2 ||
     let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
     let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-      Id.equal i1 i2 && Option.equal (eq_constr d) c1 c2 && (eq_constr d) t1 t2
+      Id.equal i1 i2 && Option.equal (eq_constr_test d) c1 c2 && (eq_constr_test d) t1 t2
     in List.equal eq_named_declaration c1 c2
 
 let eq_evar_body d b1 b2 = match b1, b2 with
 | Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr d t1 t2
+| Evar_defined t1, Evar_defined t2 -> eq_constr_test d t1 t2
 | _ -> false
 
 let eq_evar_info d ei1 ei2 =
   ei1 == ei2 ||
-    eq_constr d ei1.evar_concl ei2.evar_concl &&
+    eq_constr_test d ei1.evar_concl ei2.evar_concl &&
     eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) &&
     eq_evar_body d ei1.evar_body ei2.evar_body
     (** ppedrot: [eq_constr] may be a bit too permissive here *)