From 5184e911a4192adcfd0699a8da5bbe393cf599f3 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 15 Jun 2010 15:39:35 +0000
Subject: CHANGES: list of modifications for the extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13138 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/CHANGES b/CHANGES
index 072a298d2d..6f6510be11 100644
--- a/CHANGES
+++ b/CHANGES
@@ -127,6 +127,23 @@ Module system
   "Inline" annotation in the type of its argument(s) (for examples of
   use of the new features, see libraries Structures and Numbers).
 
+Extraction
+
+- 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
+  be preserved, let-ins are almost always kept, etc.
+- 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
+  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
+  (in this case recognition of ascii constants is hard-wired in the extraction).
+
 Program
 
 - Streamlined definitions using well-founded recursion and measures so
-- 
cgit v1.2.3