diff options
| author | Matthieu Sozeau | 2015-09-23 19:14:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:11 +0200 |
| commit | 43858a207437fa08f066bdd3cae7bcd3034808f1 (patch) | |
| tree | abc028574bdfd99b22c348e09b4ccd92c8b5e321 /library | |
| parent | c92946243ccb0b11cd138f040a5297979229c3f5 (diff) | |
Univs: fix Universe vernacular, fix bug #4287.
No universe can be set lower than Prop anymore (or Set).
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 10 |
1 files changed, 6 insertions, 4 deletions
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') |