From a0e72610a71e086da392c8563c2eec2e35211afa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 Nov 2015 17:21:35 +0100
Subject: Avoid recording spurious Set <= Top.i constraints which are always
 valid (when Top.i is global and hence > Set).

---
 library/universes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/universes.ml b/library/universes.ml
index 6cccb10efb..1b6f7a9d57 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -854,7 +854,7 @@ let normalize_context_set ctx us algs =
     Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
         if d == Le then
 	  if Univ.Level.is_small l then
-	    if is_set_minimization () then
+	    if is_set_minimization () && LSet.mem r ctx then
 	      (Constraint.add cstr smallles, noneqs)
 	    else (smallles, noneqs)
 	  else if Level.is_small r then
-- 
cgit v1.2.3