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/vconv.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/vconv.ml')

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