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

1 files changed, 4 insertions, 6 deletions

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;