diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-15 15:46:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:18:56 +0100 |
| commit | d437078a4ca82f7ca6d19be5ee9452359724f9a0 (patch) | |
| tree | 628fd2161dcc0fcfabe9499669ee932d7878b63d /interp | |
| parent | 485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf (diff) | |
Use Maps and ids for universe binders
Before sometimes there were lists and strings.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 8 |
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)) |