From d437078a4ca82f7ca6d19be5ee9452359724f9a0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 15:46:30 +0200
Subject: Use Maps and ids for universe binders

Before sometimes there were lists and strings.
---
 interp/declare.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 7ab13b8592..dc77981f2a 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -462,11 +462,11 @@ type universe_decl = polymorphic * Universes.universe_binders
 let cache_universes (p, l) =
   let glob = Global.global_universe_names () in
   let glob', ctx =
-    List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
+    Id.Map.fold (fun id lev ((idl,lid),ctx) ->
         ((Id.Map.add id (p, lev) idl,
           Univ.LMap.add lev id lid),
          Univ.ContextSet.add_universe lev ctx))
-      (glob, Univ.ContextSet.empty) l
+      l (glob, Univ.ContextSet.empty)
   in
   cache_universe_context (p, ctx);
   Global.set_global_universe_names glob'
@@ -487,9 +487,9 @@ let do_universe poly l =
                    (str"Cannot declare polymorphic universes outside sections")
   in
   let l =
-    List.map (fun (l, id) ->
+    List.fold_left (fun acc (l, id) ->
 	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
-	      (id, lev)) l
+              Id.Map.add id lev acc) Id.Map.empty l
   in
     Lib.add_anonymous_leaf (input_universes (poly, l))
 
-- 
cgit v1.2.3