From a27c212a0fc5fd8e28c958f0c76f1768f3f95044 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 15 Sep 2011 09:10:46 +0000
Subject: Names.make_mbid and co : convert from/to identifier (avoid some
 String.copy)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14468 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declaremods.ml | 2 +-
 library/lib.ml         | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 8753624a9d..d4712762ac 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -545,7 +545,7 @@ let process_module_seb_binding mbid seb =
 let intern_args interp_modtype (idl,(arg,ann)) =
   let inl = inline_annot ann in
   let lib_dir = Lib.library_dp() in
-  let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
+  let mbids = List.map (fun (_,id) -> make_mbid lib_dir id) idl in
   let mty = interp_modtype (Global.env()) arg in
   let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
   let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env())
diff --git a/library/lib.ml b/library/lib.ml
index cfaea3b663..23d334a5dc 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -728,7 +728,7 @@ let rec split_mp mp =
     | Names.MPdot (prfx, lbl) ->
 	let mprec, dprec = split_mp prfx in
 	  mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
-    | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
+    | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [id]
 
 let split_modpath mp =
   let rec aux = function
-- 
cgit v1.2.3