Modulification of Label

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7

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