From 2d6de8b102ea3cd05c5d193190faf787ccb84baa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 17:29:26 +0200
Subject: Fix restrict_universe_context removing some universes that do appear
 in the term.

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

(limited to 'library')

diff --git a/library/universes.ml b/library/universes.ml
index 2ed477d67b..7d1908d1f5 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -673,7 +673,7 @@ let restrict_universe_context (univs,csts) s =
         if LSet.mem l diff && LSet.mem r diff then (univs, csts)
 	else (LSet.add l (LSet.add r univs), Constraint.add c csts))
     csts (LSet.empty, Constraint.empty)
-  in (LSet.inter univs univscstrs, csts)
+  in (LSet.union s (LSet.inter univs univscstrs), csts)
 
 let simplify_universe_context (univs,csts) =
   let uf = UF.create () in
-- 
cgit v1.2.3