Extraction Library works now when some files share the same short name (fix #2025)

 For instance, when we need to extract Init.Wf and Program.Wf,
 the first one gives wf.ml and the second wf0.ml.

 This name resolution mechanism is merged with the handling of the
 extraction filename blacklist. Hence, after Extraction Blacklist Foo,
 the coq file Foo.v will now be extracted as foo0.ml (instead of
 coq_Foo.ml as previously).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11843 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 11 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index e2cd2e465f..401ca1e55b 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -346,16 +346,11 @@ let mono_filename f =
 
 (* Builds a suitable filename from a module id *)
 
-let module_filename m =
+let module_filename fc =
   let d = descr () in
-  let fc = String.capitalize (string_of_id m) in
-  let fn =
-    if is_blacklisted fc then
-      if d.capital_file then "Coq_"^fc else "coq_"^fc
-    else
-      if d.capital_file then fc else String.uncapitalize fc
+  let fn = if d.capital_file then fc else String.uncapitalize fc
   in
-  Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, m
+  Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, id_of_string fc
 
 (*s Extraction of one decl to stdout. *)
 
@@ -513,10 +508,10 @@ let extraction_library is_rec m =
   let struc = optimize_struct [] struc in
   warning_axioms ();
   let print = function
-    | (MPfile dir, sel) as e ->
+    | (MPfile dir as mp, sel) as e ->
 	let dry = not is_rec && dir <> dir_m in
-	let short_m = snd (split_dirpath dir) in
-	print_structure_to_file (module_filename short_m) dry [e]
+	let s = string_of_modfile mp in
+	print_structure_to_file (module_filename s) dry [e]
     | _ -> assert false
   in
   List.iter print struc;