From fd06eda492de2566ae44777ddbc9cd32744a2633 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 6 Jun 2014 15:59:38 +0200
Subject: 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).

---
 kernel/constr.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/constr.mli')

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]. *)
-- 
cgit v1.2.3