From 2be0079f2ed4b67eae474341a10b9f60dcf83c4f Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 7 Jul 2010 14:01:59 +0000 Subject: Extraction Library Foo creates Foo.ml, not foo.ml And similarly for Haskell: we do not force capitalized/uncapitalized filenames anymore, but we rather follow the name of the .v file (with new extensions of course). Ok, this is an incompatible change, but it is really convenient, some people where actually already doing some hacks to have this behavior (cf. Compcert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13260 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/extract_env.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'plugins/extraction/extract_env.ml') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index b1195b4be5..db7504e3eb 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -370,11 +370,10 @@ let mono_filename f = (* Builds a suitable filename from a module id *) -let module_filename fc = +let module_filename mp = + let f = file_of_modfile mp in let d = descr () in - let fn = if d.capital_file then fc else String.uncapitalize fc - in - Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, id_of_string fc + Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f (*s Extraction of one decl to stdout. *) @@ -531,8 +530,7 @@ let extraction_library is_rec m = let print = function | (MPfile dir as mp, sel) as e -> let dry = not is_rec && dir <> dir_m in - let s = string_of_modfile mp in - print_structure_to_file (module_filename s) dry [e] + print_structure_to_file (module_filename mp) dry [e] | _ -> assert false in List.iter print struc; -- cgit v1.2.3