diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-21 11:14:11 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
| commit | d071eac98b7812ac5c03004b438022900885d874 (patch) | |
| tree | f0f72dba7daf7c91ea2eda0332b568c4615ad3c9 /engine/universes.ml | |
| parent | 765392492df2f5e065b2b5e706b6620846337cc0 (diff) | |
Forbid repeated names in universe binders.
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 |