diff options
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index f2942be6d..5ac1bc685 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -55,7 +55,7 @@ let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj let register_universe_binders ref ubinders = (* Add the polymorphic (section) universes *) let open Names in - let ubinders = Idmap.fold (fun id (poly,lvl) ubinders -> + let ubinders = Id.Map.fold (fun id (poly,lvl) ubinders -> if poly then Id.Map.add id lvl ubinders else ubinders) (fst (Global.global_universe_names ())) ubinders |