Modulification of Label

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

6 files changed, 22 insertions, 22 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index eaca147e1..5ef789561 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -328,9 +328,9 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q =
               Parameter*)
       (
         let mp,dir,lbl = repr_con (destConst v) in
-          mkConst (make_con mp dir (mk_label (
-          if Int.equal offset 1 then ("eq_"^(string_of_label lbl))
-                       else ((string_of_label lbl)^"_lb")
+          mkConst (make_con mp dir (Label.make (
+          if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
+                       else ((Label.to_string lbl)^"_lb")
         )))
       )
   in
@@ -375,9 +375,9 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
               Parameter*)
       (
         let mp,dir,lbl = repr_con (destConst v) in
-          mkConst (make_con mp dir (mk_label (
-          if Int.equal offset 1 then ("eq_"^(string_of_label lbl))
-                       else ((string_of_label lbl)^"_bl")
+          mkConst (make_con mp dir (Label.make (
+          if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
+                       else ((Label.to_string lbl)^"_bl")
         )))
       )
   in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 01205e597..6f0ac1793 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -164,8 +164,8 @@ let get_strength stre ref cls clt =
 let ident_key_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
-  | CL_CONST sp -> string_of_label (con_label sp)
-  | CL_IND (sp,_) -> string_of_label (mind_label sp)
+  | CL_CONST sp -> Label.to_string (con_label sp)
+  | CL_IND (sp,_) -> Label.to_string (mind_label sp)
   | CL_SECVAR id -> Id.to_string id
 
 (* coercion identité *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index fbabaa432..a5805b637 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -85,7 +85,7 @@ let refine_ref = ref (fun _ -> assert(false))
 
 let id_of_class cl =
   match cl.cl_impl with
-    | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
+    | ConstRef kn -> let _,_,l = repr_con kn in Label.to_id l
     | IndRef (kn,i) ->
 	let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
 	  mip.(0).Declarations.mind_typename
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ef510aee5..8289f6ca2 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -572,11 +572,11 @@ let explain_not_match_error = function
     strbrk "a definition whose type is constrained can only be subtype of a definition whose type is itself constrained"
 
 let explain_signature_mismatch l spec why =
-  str "Signature components for label " ++ str (string_of_label l) ++
+  str "Signature components for label " ++ str (Label.to_string l) ++
   str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "."
 
 let explain_label_already_declared l =
-  str ("The label "^string_of_label l^" is already declared.")
+  str ("The label "^Label.to_string l^" is already declared.")
 
 let explain_application_to_not_path _ =
   str "Application of modules is restricted to paths."
@@ -591,11 +591,11 @@ let explain_not_equal_module_paths mp1 mp2 =
   str "Non equal modules."
 
 let explain_no_such_label l =
-  str "No such label " ++ str (string_of_label l) ++ str "."
+  str "No such label " ++ str (Label.to_string l) ++ str "."
 
 let explain_incompatible_labels l l' =
   str "Opening and closing labels are not the same: " ++
-  str (string_of_label l) ++ str " <> " ++ str (string_of_label l') ++ str "!"
+  str (Label.to_string l) ++ str " <> " ++ str (Label.to_string l') ++ str "!"
 
 let explain_signature_expected mtb =
   str "Signature expected."
@@ -613,24 +613,24 @@ let explain_not_a_module_type s =
   quote (str s) ++ str " is not a module type."
 
 let explain_not_a_constant l =
-  quote (pr_label l) ++ str " is not a constant."
+  quote (Label.print l) ++ str " is not a constant."
 
 let explain_incorrect_label_constraint l =
   str "Incorrect constraint for label " ++
-  quote (pr_label l) ++ str "."
+  quote (Label.print l) ++ str "."
 
 let explain_generative_module_expected l =
-  str "The module " ++ str (string_of_label l) ++
+  str "The module " ++ str (Label.to_string l) ++
   strbrk " is not generative. Only components of generative modules can be changed using the \"with\" construct."
 
 let explain_non_empty_local_context = function
   | None -> str "The local context is not empty."
   | Some l ->
       str "The local context of the component " ++
-      str (string_of_label l) ++ str " is not empty."
+      str (Label.to_string l) ++ str " is not empty."
 
 let explain_label_missing l s =
-  str "The field " ++ str (string_of_label l) ++ str " is missing in "
+  str "The field " ++ str (Label.to_string l) ++ str " is missing in "
   ++ str s ++ str "."
 
 let explain_module_error = function
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f37d99dd1..2a9af66ff 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -268,7 +268,7 @@ let print_namespace ns =
     | MPbound _ -> None (* Not a proper namespace. *)
     | MPfile dir -> match_dirpath ns (Names.Dir_path.repr dir)
     | MPdot (mp,lbl) ->
-        let id = Names.id_of_label lbl in
+        let id = Names.Label.to_id lbl in
         begin match match_modulepath ns mp with
         | Some [] as y -> y
         | Some (a::ns') ->
@@ -287,7 +287,7 @@ let print_namespace ns =
     let rec list_of_modulepath = function
       | MPbound _ -> assert false (* MPbound never matches *)
       | MPfile dir -> Names.Dir_path.repr dir
-      | MPdot (mp,lbl) -> (Names.id_of_label lbl)::(list_of_modulepath mp)
+      | MPdot (mp,lbl) -> (Names.Label.to_id lbl)::(list_of_modulepath mp)
     in
     snd (Util.List.chop n (List.rev (list_of_modulepath mp)))
   in
@@ -295,7 +295,7 @@ let print_namespace ns =
   let print_kn kn =
     (* spiwack: I'm ignoring the dirpath, is that bad? *)
     let (mp,_,lbl) = Names.repr_kn kn in
-    let qn = (qualified_minus (List.length ns) mp)@[Names.id_of_label lbl] in
+    let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
     print_list pr_id qn
   in
   let print_constant k body =
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 4999cd0c2..935606fc4 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -83,7 +83,7 @@ let error_whelp_unknown_reference ref =
 let uri_of_repr_kn ref (mp,dir,l) =
   match mp with
     | MPfile sl ->
-        uri_of_dirpath (id_of_label l :: Dir_path.repr dir @ Dir_path.repr sl)
+        uri_of_dirpath (Label.to_id l :: Dir_path.repr dir @ Dir_path.repr sl)
     | _ ->
         error_whelp_unknown_reference ref