diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-15 09:10:46 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-15 09:10:46 +0000 |
commit | a27c212a0fc5fd8e28c958f0c76f1768f3f95044 (patch) | |
tree | 64ed90829db9de6fcff1a816c24f5fcd6da5cfbb /library/declaremods.ml | |
parent | 03b99149b5ab569be43d6cb3d34fb4766931074d (diff) |
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
Diffstat (limited to 'library/declaremods.ml')
-rw-r--r-- | library/declaremods.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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()) |