diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-07 14:01:59 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-07 14:01:59 +0000 |
commit | 2be0079f2ed4b67eae474341a10b9f60dcf83c4f (patch) | |
tree | 97e03cde10cff22588e9019477d16febb93fc75e /plugins/extraction/miniml.mli | |
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/miniml.mli')
-rw-r--r-- | plugins/extraction/miniml.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index a1e59e2a0..a27a9cf03 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -178,7 +178,6 @@ type language_descr = { (* Concerning the source file *) file_suffix : string; - capital_file : bool; (* should we capitalize filenames ? *) preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; pp_struct : ml_structure -> std_ppcmds; |