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).

1 files changed, 2 insertions, 2 deletions

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 8e623415e7..0e91c79727 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -50,7 +50,7 @@ let rec conv_val pb k v1 v2 cu =
 
 and conv_whd pb k whd1 whd2 cu =
   match whd1, whd2 with
-  | Vsort s1, Vsort s2 -> ignore(sort_cmp_universes pb s1 s2 (cu,None)); cu
+  | Vsort s1, Vsort s2 -> check_sort_cmp_universes pb s1 s2 cu; cu
   | Vprod p1, Vprod p2 ->
       let cu = conv_val CONV k (dom p1) (dom p2) cu in
       conv_fun pb k (codom p1) (codom p2) cu
@@ -188,7 +188,7 @@ let rec conv_eq pb t1 t2 cu =
 	if Int.equal m1 m2 then cu else raise NotConvertible
     | Var id1, Var id2 ->
 	if Id.equal id1 id2 then cu else raise NotConvertible
-    | Sort s1, Sort s2 -> ignore(sort_cmp_universes pb s1 s2 (cu,None)); cu
+    | Sort s1, Sort s2 -> check_sort_cmp_universes pb s1 s2 cu; cu
     | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu
     | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu
     | Prod (_,t1,c1), Prod (_,t2,c2) ->