diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index dbc5b01f1..c15681b04 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -45,36 +45,36 @@ let add_mib_nameobjects mp l mib map = let map = Array.fold_right_i (fun i id map -> - Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) + Label.Map.add (Label.of_id id) (IndConstr((ip,i+1), mib)) map) oib.mind_consnames map in - Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map + Label.Map.add (Label.of_id oib.mind_typename) (IndType (ip, mib)) map in Array.fold_right_i add_mip_nameobjects mib.mind_packets map (* creates (namedobject/namedmodule) map for the whole signature *) -type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t } +type labmap = { objs : namedobject Label.Map.t; mods : namedmodule Label.Map.t } -let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty } +let empty_labmap = { objs = Label.Map.empty; mods = Label.Map.empty } let get_obj mp map l = - try Labmap.find l map.objs + try Label.Map.find l map.objs with Not_found -> error_no_such_label_sub l (string_of_mp mp) let get_mod mp map l = - try Labmap.find l map.mods + try Label.Map.find l map.mods with Not_found -> error_no_such_label_sub l (string_of_mp mp) let make_labmap mp list = let add_one (l,e) map = match e with - | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs } + | SFBconst cb -> { map with objs = Label.Map.add l (Constant cb) map.objs } | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs } - | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods } - | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods } + | SFBmodule mb -> { map with mods = Label.Map.add l (Module mb) map.mods } + | SFBmodtype mtb -> { map with mods = Label.Map.add l (Modtype mtb) map.mods } in List.fold_right add_one list empty_labmap |