1 files changed, 14 insertions, 14 deletions
diff --git a/library/nameops.ml b/library/nameops.ml
index 461e7a405..f8f95135f 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -12,7 +12,7 @@ open Names
 
 (* Identifiers *)
 
-let pr_id id = str (string_of_id id)
+let pr_id id = str (Id.to_string id)
 
 let pr_name = function
   | Anonymous -> str "_"
@@ -24,7 +24,7 @@ let code_of_0 = Char.code '0'
 let code_of_9 = Char.code '9'
 
 let cut_ident skip_quote s =
-  let s = string_of_id s in
+  let s = Id.to_string s in
   let slen = String.length s in
   (* [n'] is the position of the first non nullary digit *)
   let rec numpart n n' =
@@ -46,7 +46,7 @@ let cut_ident skip_quote s =
 
 let repr_ident s =
   let numstart = cut_ident false s in
-  let s = string_of_id s in
+  let s = Id.to_string s in
   let slen = String.length s in
   if Int.equal numstart slen then
     (s, None)
@@ -60,17 +60,17 @@ let make_ident sa = function
       let s =
         if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n)
         else sa ^ "_" ^ (string_of_int n) in
-      id_of_string s
-  | None -> id_of_string (String.copy sa)
+      Id.of_string s
+  | None -> Id.of_string (String.copy sa)
 
 let root_of_id id =
   let suffixstart = cut_ident true id in
-  id_of_string (String.sub (string_of_id id) 0 suffixstart)
+  Id.of_string (String.sub (Id.to_string id) 0 suffixstart)
 
 (* Rem: semantics is a bit different, if an ident starts with toto00 then
   after successive renamings it comes to toto09, then it goes on with toto10 *)
 let lift_subscript id =
-  let id = string_of_id id in
+  let id = Id.to_string id in
   let len = String.length id in
   let rec add carrypos =
     let c = id.[carrypos] in
@@ -93,20 +93,20 @@ let lift_subscript id =
       end;
       newid
     end
-  in id_of_string (add (len-1))
+  in Id.of_string (add (len-1))
 
 let has_subscript id =
-  let id = string_of_id id in
+  let id = Id.to_string id in
   is_digit (id.[String.length id - 1])
 
 let forget_subscript id =
   let numstart = cut_ident false id in
   let newid = String.make (numstart+1) '0' in
-  String.blit (string_of_id id) 0 newid 0 numstart;
-  (id_of_string newid)
+  String.blit (Id.to_string id) 0 newid 0 numstart;
+  (Id.of_string newid)
 
-let add_suffix id s = id_of_string (string_of_id id ^ s)
-let add_prefix s id = id_of_string (s ^ string_of_id id)
+let add_suffix id s = Id.of_string (Id.to_string id ^ s)
+let add_prefix s id = Id.of_string (s ^ Id.to_string id)
 
 let atompart_of_id id = fst (repr_ident id)
 
@@ -141,7 +141,7 @@ let pr_lab l = str (string_of_label l)
 let default_library = Names.initial_dir (* = ["Top"] *)
 
 (*s Roots of the space of absolute names *)
-let coq_root = id_of_string "Coq"
+let coq_root = Id.of_string "Coq"
 let default_root_prefix = make_dirpath []
 
 (* Metavariables *)