aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/miniml.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-07 14:01:59 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-07 14:01:59 +0000
commit2be0079f2ed4b67eae474341a10b9f60dcf83c4f (patch)
tree97e03cde10cff22588e9019477d16febb93fc75e /plugins/extraction/miniml.mli
parent670a61a7ca4c55a5e06a79a73989a52bf0cb2273 (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.mli1
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;