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/nativeconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativeconv.ml')

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 766e6513c7..5964ed70ed 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -70,7 +70,7 @@ and conv_atom pb lvl a1 a2 cu =
 	if not (eq_constant c1 c2) then raise NotConvertible;
 	cu
     | Asort s1, Asort s2 -> 
-	ignore(sort_cmp_universes pb s1 s2 (cu, None)); cu
+        check_sort_cmp_universes pb s1 s2 cu; cu
     | Avar id1, Avar id2 ->
 	if not (Id.equal id1 id2) then raise NotConvertible;
 	cu
-- 
cgit v1.2.3