diff options
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index c6eacc289..fbcdc886b 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -577,6 +577,52 @@ let leq_constr_univs univs m n = and leq_constr' m n = m == n || compare_leq m n in compare_leq m n +let eq_constr_univs_infer univs m n = + if m == n then true, Constraint.empty + else + let cstrs = ref Constraint.empty in + let eq_universes strict = Univ.Instance.check_eq univs in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + (cstrs := Univ.enforce_eq u1 u2 !cstrs; + true) + in + let rec eq_constr' m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in + res, !cstrs + +let leq_constr_univs_infer univs m n = + if m == n then true, Constraint.empty + else + let cstrs = ref Constraint.empty in + let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + (cstrs := Univ.enforce_eq u1 u2 !cstrs; + true) + in + let leq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + (cstrs := Univ.enforce_leq u1 u2 !cstrs; + true) + in + let rec eq_constr' m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let rec compare_leq m n = + compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n + and leq_constr' m n = m == n || compare_leq m n in + let res = compare_leq m n in + res, !cstrs + let eq_constr_universes m n = if m == n then true, UniverseConstraints.empty else |