From c1cd47d5dff18f12af063d2c8defbd985c97dec6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 14 Nov 2013 11:50:04 +0100
Subject: - Fix comparison of universes. - Shortcut for Set <= x checks,
 assuming that this is always true except when x (or rather its canonical
 representative) is Prop. Invariant to check. - Uncomment the profiling code
 and make it depend on a (statically known) boolean.

---
 library/universes.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/universes.ml b/library/universes.ml
index b31aab1988..99c8b39f95 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -638,6 +638,9 @@ let restrict_universe_context (univs,csts) s =
       csts Constraint.empty
   in (univs', csts')
 
+let is_small_leq (l,d,r) =
+  Level.is_small l && d == Univ.Le
+
 let is_prop_leq (l,d,r) =
   Level.equal Level.prop l && d == Univ.Le
 
@@ -651,7 +654,7 @@ let refresh_constraints univs (ctx, cstrs) =
   let cstrs', univs' = 
     Univ.Constraint.fold (fun c (cstrs', univs as acc) -> 
       let c = translate_cstr c in
-      if Univ.check_constraint univs c && not (is_prop_leq c) then acc
+      if Univ.check_constraint univs c && not (is_small_leq c) then acc
       else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
       cstrs (Univ.Constraint.empty, univs)
   in ((ctx, cstrs'), univs')
-- 
cgit v1.2.3