diff options
| author | letouzey | 2010-07-07 14:01:59 +0000 |
|---|---|---|
| committer | letouzey | 2010-07-07 14:01:59 +0000 |
| commit | 2be0079f2ed4b67eae474341a10b9f60dcf83c4f (patch) | |
| tree | 97e03cde10cff22588e9019477d16febb93fc75e /plugins/extraction/table.ml | |
| parent | 670a61a7ca4c55a5e06a79a73989a52bf0cb2273 (diff) | |
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
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 8 |
1 files changed, 8 insertions, 0 deletions
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))) |