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 | |
| 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')
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/lib.ml | 2 |
2 files changed, 2 insertions, 2 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()) diff --git a/library/lib.ml b/library/lib.ml index cfaea3b66..23d334a5d 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 |