From 43858a207437fa08f066bdd3cae7bcd3034808f1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 19:14:05 +0200
Subject: Univs: fix Universe vernacular, fix bug #4287.

No universe can be set lower than Prop anymore (or Set).
---
 library/declare.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 8438380c9c..8908a2c919 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -455,12 +455,14 @@ let input_universes : universe_names -> Libobject.obj =
 
 let do_universe l =
   let glob = Universes.global_universe_names () in
-  let glob' = 
-    List.fold_left (fun (idl,lid) (l, id) ->
+  let glob', ctx = 
+    List.fold_left (fun ((idl,lid),ctx) (l, id) ->
       let lev = Universes.new_univ_level (Global.current_dirpath ()) in
-	(Idmap.add id lev idl, Univ.LMap.add lev id lid))
-      glob l
+        ((Idmap.add id lev idl, Univ.LMap.add lev id lid),
+	 Univ.ContextSet.add_universe lev ctx))
+      (glob, Univ.ContextSet.empty) l
   in
+    Global.push_context_set ctx;
     Lib.add_anonymous_leaf (input_universes glob')
 
 
-- 
cgit v1.2.3