From da88175778d6055d1ecf40c8f429cf855a4304cb Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 14 Apr 2014 17:20:22 +0200
Subject: Avoid u+k <= v constraints, don't take the sup of an algebraic
 universe during minimization.

---
 library/universes.ml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

(limited to 'library')

diff --git a/library/universes.ml b/library/universes.ml
index b0a610700e..6799a99e5b 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -463,16 +463,19 @@ exception Stays
 let compute_lbound left =
  (** The universe variable was not fixed yet.
      Compute its level using its lower bound. *)
-  if CList.is_empty left then None
-  else
-    let lbound = List.fold_left (fun lbound (d, l) -> 
-      if d == Le (* l <= ?u *) then (Universe.sup l lbound)
+  let sup l lbound = 
+    match lbound with
+    | None -> Some l
+    | Some l' -> Some (Universe.sup l l')
+  in
+    List.fold_left (fun lbound (d, l) -> 
+      if d == Le (* l <= ?u *) then sup l lbound
       else (* l < ?u *) 
 	(assert (d == Lt); 
-	 (Universe.sup (Universe.super l) lbound)))	    
-      Universe.type0m left
-    in 
-      Some lbound
+	 if not (Universe.level l == None) then
+	   sup (Universe.super l) lbound
+	 else None))
+      None left
   
 let maybe_enforce_leq lbound u cstrs = 
   match lbound with
-- 
cgit v1.2.3