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 /CHANGES | |
| 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 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -134,6 +134,9 @@ Module system Extraction +- When using (Recursive) Extraction Library, the filenames are directly the + Coq ones with new appropriate extensions : we do not force anymore + uncapital first letters for Ocaml and capital ones for Haskell. - The extraction now tries harder to avoid code transformations that can be dangerous for the complexity. In particular many eta-expansions at the top of functions body are now avoided, clever partial applications will likely |