diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-06 19:09:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-06 20:09:06 +0200 |
| commit | 84add29c036735ceacde73ea98a9a5a454a5e3a0 (patch) | |
| tree | baee8c0b023277d43366996685503c9d1f855413 /kernel/constr.ml | |
| parent | c4db6fc1086d984fd983ff9a6797ad108d220b98 (diff) | |
Splitting kernel universe code in two modules.
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index e2b1d3fd9..753d18845 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -545,8 +545,8 @@ let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = if m == n then true else - let eq_universes _ = Univ.Instance.check_eq univs in - let eq_sorts s1 s2 = s1 == s2 || Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + let eq_universes _ = UGraph.check_eq_instances univs in + let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n in compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -554,11 +554,11 @@ let eq_constr_univs univs m n = let leq_constr_univs univs m n = if m == n then true else - let eq_universes _ = Univ.Instance.check_eq univs in + let eq_universes _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || - Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let leq_sorts s1 s2 = s1 == s2 || - Univ.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + UGraph.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n in @@ -571,12 +571,12 @@ 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_universes strict = UGraph.check_eq_instances 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 - if Univ.check_eq univs u1 u2 then true + if UGraph.check_eq univs u1 u2 then true else (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) @@ -591,12 +591,12 @@ 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_universes strict l l' = UGraph.check_eq_instances 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 - if Univ.check_eq univs u1 u2 then true + if UGraph.check_eq univs u1 u2 then true else (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) in @@ -604,7 +604,7 @@ let leq_constr_univs_infer univs m n = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then true + if UGraph.check_leq univs u1 u2 then true else (cstrs := Univ.enforce_leq u1 u2 !cstrs; true) |