From 4bfb3331804fd191a1d5fb92e99ae17b080f4f7b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 8 Apr 2014 15:59:36 +0200
Subject: Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.

---
 pretyping/evd.ml | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

(limited to 'pretyping/evd.ml')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index fd6af80b89..652bed5a36 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -373,10 +373,11 @@ let process_universe_constraints univs vars alg local cstrs =
 	      match Univ.Universe.level r with
 	      | None -> error ("Algebraic universe on the right")
 	      | Some rl when Univ.Level.is_small rl -> 
-		(match Univ.Universe.level l with
-		| Some ll when Univ.LMap.mem ll !vars -> 
-		  Univ.enforce_eq l r local
-		| _ -> raise (Univ.UniverseInconsistency (Univ.Le, l, r, [])))
+		(if Univ.LSet.for_all (fun l -> 
+		  Univ.Level.is_small l || Univ.LMap.mem l !vars) 
+		    (Univ.Universe.levels l) then
+		    Univ.enforce_leq l r local
+		 else raise (Univ.UniverseInconsistency (Univ.Le, l, r, [])))
 	      | _ -> Univ.enforce_leq l r local
 	  else if d == Univ.ULub then
 	    match varinfo l, varinfo r with
@@ -1112,11 +1113,6 @@ let set_leq_sort evd s1 s2 =
       | Prop c, Prop c' -> 
 	  if c == Null && c' == Pos then evd
 	  else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])))
-      | Type u, Prop _ ->
-	(match is_sort_variable evd s1 with
-	| Some (_, false) -> 
-	  add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1, Univ.UEq, u2))
-	| _ -> raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])))
       | _, _ ->
         add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2))
 	
-- 
cgit v1.2.3