aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-15 15:46:30 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-24 19:18:56 +0100
commitd437078a4ca82f7ca6d19be5ee9452359724f9a0 (patch)
tree628fd2161dcc0fcfabe9499669ee932d7878b63d /interp
parent485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf (diff)
Use Maps and ids for universe binders
Before sometimes there were lists and strings.
Diffstat (limited to 'interp')
-rw-r--r--interp/declare.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/declare.ml b/interp/declare.ml
index 7ab13b859..dc77981f2 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))