From d071eac98b7812ac5c03004b438022900885d874 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 21 Sep 2017 11:14:11 +0200
Subject: Forbid repeated names in universe binders.

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

(limited to 'engine/universes.ml')

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
-- 
cgit v1.2.3