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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index bb20dc7fc..b1ba16b5c 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -260,7 +260,7 @@ let pr_module_vardecls pr_c (export,idl,(mty,inl)) = let lib_dir = Lib.library_dp() in List.iter (fun (_,id) -> Declaremods.process_module_bindings [id] - [make_mbid lib_dir (string_of_id id), + [make_mbid lib_dir id, (Modintern.interp_modtype (Global.env()) mty, inl)]) idl; (* Builds the stream *) spc() ++ |