diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index e49ed7b45..63e25a541 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1333,35 +1333,36 @@ let test_conversion env d pb t u = try conversion_gen env d pb t u; true with _ -> false -let eq_constr evd t u = +let eq_constr_univs 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 +let e_eq_constr_univs evdref t u = + let evd, b = eq_constr_univs !evdref t u in evdref := evd; b -let eq_constr_test evd t u = - snd (eq_constr evd t u) +let eq_constr_univs_test evd t u = + snd (eq_constr_univs 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_test d) c1 c2 && (eq_constr_test d) t1 t2 + Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2 + && (eq_constr_univs_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_test d t1 t2 +| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2 | _ -> false let eq_evar_info d ei1 ei2 = ei1 == ei2 || - eq_constr_test d ei1.evar_concl ei2.evar_concl && + eq_constr_univs_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 *) |