diff options
| author | Matthieu Sozeau | 2014-06-06 15:59:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-06 16:07:08 +0200 |
| commit | fd06eda492de2566ae44777ddbc9cd32744a2633 (patch) | |
| tree | ba76c5e2fe20e04cde3766a0401be0fe3e3ccdb0 /kernel/constr.mli | |
| parent | 3b83b311798f0d06444e1994602e0b531e207ef5 (diff) | |
Make kernel reduction code parametric over the handling of universes,
allowing fast conversion to be used during unification while respecting the
semantics of unification w.r.t universes.
- Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv
is used for module subtyping.
- Outside, infer_conv is wrapped in Reductionops to register the right constraints
in an evarmap.
- In univ, add a flag to universes to cache the fact that they are >= Set, the
most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index e9f7369034..c57c4c59b2 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -212,11 +212,11 @@ val leq_constr_univs : constr Univ.check_function (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, application grouping and the universe equalities in [u]. *) -val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained +val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.universe_constrained (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe inequalities in [u]. *) -val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained +val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.universe_constrained (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe equalities in [c]. *) |