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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/declaremods.ml') diff --git a/library/declaremods.ml b/library/declaremods.ml index 8753624a9..d4712762a 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()) -- cgit v1.2.3