diff options
| author | letouzey | 2010-07-07 08:34:38 +0000 |
|---|---|---|
| committer | letouzey | 2010-07-07 08:34:38 +0000 |
| commit | 670a61a7ca4c55a5e06a79a73989a52bf0cb2273 (patch) | |
| tree | d229962e10358431a224dab51eff3bcf1b8a28be | |
| parent | f09085bb59dc82c62ebd000f72cbbc3d59e3cc6b (diff) | |
CHANGES: mention last-minute improvements of extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13250 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 9 |
1 files changed, 7 insertions, 2 deletions
@@ -138,12 +138,17 @@ Extraction dangerous for the complexity. In particular many eta-expansions at the top of functions body are now avoided, clever partial applications will likely be preserved, let-ins are almost always kept, etc. +- Harsh support of module extraction to Haskell and Scheme: module hierarchy + is flattened, module abbreviations and functor applications are expanded, + module types and unapplied functors are discarded. +- Less unsupported situations when extracting modules to Ocaml. In particular + module parameters might be alpha-renamed if a name clash is detected. - Extract Inductive is now possible toward non-inductive types (e.g. nat => int) - Extraction Implicit: this new experimental command allows to mark some arguments of a function or constructor for removed during extraction, even if these arguments don't fit the usual elimination principles of extraction, for instance the length n of a vector. -- A few .v files in plugins/extraction try to provide a library of common +- Files ExtrOcaml*.v in plugins/extraction try to provide a library of common extraction commands: mapping of basics types toward Ocaml's counterparts, conversions from/to int and big_int, or even complete mapping of nat,Z,N to int or big_int, or mapping of ascii to char and string to char list @@ -258,7 +263,7 @@ Library - Numbers library: - The abstract layer (NatInt, Natural/Abstract, Integer/Abstract) has been simplified and enhance thanks to new features of the module - system such as Include (see below). It has been extended to Euclidean + system such as Include (see above). It has been extended to Euclidean division (three flavors for integers: Trunc, Floor and Math). - The arbitrary-large efficient numbers (BigN, BigZ, BigQ) has also been reworked. They benefit from the abstract layer improvements |