Modulification of Label

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

4 files changed, 21 insertions, 21 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 548dd32fc..d354eb8c4 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -21,19 +21,19 @@ open Environ
 let rec debug_string_of_mp = function
   | MPfile sl -> Dir_path.to_string sl
   | MPbound uid -> "bound("^string_of_mbid uid^")"
-  | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ string_of_label l
+  | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ Label.to_string l
 
 let rec string_of_mp = function
   | MPfile sl -> Dir_path.to_string sl
   | MPbound uid -> string_of_mbid uid
-  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ Label.to_string l
 
 let string_of_mp mp =
   if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
 
 let prkn kn =
   let (mp,_,l) = repr_kn kn in
-  str(string_of_mp mp ^ "." ^ string_of_label l)
+  str(string_of_mp mp ^ "." ^ Label.to_string l)
 let prcon c =
   let ck = canonical_con c in
   let uk = user_con c in
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index b8e5fa043..fa1b26cc5 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -152,7 +152,7 @@ and check_with_def env mtb (idl,c) mp =
     | [] -> assert false
     | id::idl -> id,idl
   in
-  let l = label_of_id id in
+  let l = Label.of_id id in
     try
       let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
       let before = List.rev rev_before in
@@ -189,7 +189,7 @@ and check_with_mod env mtb (idl,mp1) mp =
     | [] -> assert false
     | id::idl -> id,idl
   in
-  let l = label_of_id id in
+  let l = Label.of_id id in
     try
       let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in
       let before = List.rev rev_before in
diff --git a/checker/modops.ml b/checker/modops.ml
index 4330eff30..f9c52c2e9 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -16,32 +16,32 @@ open Declarations
 (*i*)
 
 let error_not_a_constant l =
-  error ("\""^(string_of_label l)^"\" is not a constant")
+  error ("\""^(Label.to_string l)^"\" is not a constant")
 
 let error_not_a_functor _ = error "Application of not a functor"
 
 let error_incompatible_modtypes _ _ = error "Incompatible module types"
 
 let error_not_match l _ =
-  error ("Signature components for label "^string_of_label l^" do not match")
+  error ("Signature components for label "^Label.to_string l^" do not match")
 
-let error_no_such_label l = error ("No such label "^string_of_label l)
+let error_no_such_label l = error ("No such label "^Label.to_string l)
 
 let error_no_such_label_sub l l1 =
   let l1 = string_of_mp l1 in
   error ("The field "^
-         string_of_label l^" is missing in "^l1^".")
+         Label.to_string l^" is missing in "^l1^".")
 
 let error_not_a_module_loc loc s =
-  user_err_loc (loc,"",str ("\""^string_of_label s^"\" is not a module"))
+  user_err_loc (loc,"",str ("\""^Label.to_string s^"\" is not a module"))
 
 let error_not_a_module s = error_not_a_module_loc Loc.ghost s
 
 let error_with_incorrect l =
-  error ("Incorrect constraint for label \""^(string_of_label l)^"\"")
+  error ("Incorrect constraint for label \""^(Label.to_string l)^"\"")
 
 let error_a_generative_module_expected l =
-  error ("The module " ^ string_of_label l ^ " is not generative. Only " ^
+  error ("The module " ^ Label.to_string l ^ " is not generative. Only " ^
          "component of generative modules can be changed using the \"with\" " ^
          "construct.")
 
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 951bed6c1..b23043a37 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -41,36 +41,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 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 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