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/table.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'plugins/extraction/table.ml') diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 439bb2a56f..301b6ed501 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -600,6 +600,14 @@ let string_of_modfile mp = modfile_mps := MPmap.add mp s' !modfile_mps; s' +(* same as [string_of_modfile], but preserves the capital/uncapital 1st char *) + +let file_of_modfile mp = + let s0 = raw_string_of_modfile mp in + let s = string_of_modfile mp in + if s.[0] <> s0.[0] then s.[0] <- s0.[0]; + s + let add_blacklist_entries l = blacklist_table := List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s))) -- cgit v1.2.3