From cba0e91d314c955aa9ece7c195193020e93a460f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 8 Oct 2010 07:57:38 +0000
Subject: update CHANGES w.r.t. extraction

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

diff --git a/CHANGES b/CHANGES
index 3f0574762d..6f58e6c314 100644
--- a/CHANGES
+++ b/CHANGES
@@ -144,6 +144,12 @@ 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.
+- In the same spirit, auto-inlining is now disabled by default, except for
+  induction principles, since this feature was producing more frequently
+  weird code than clear gain. The previous behavior can be restored via
+  "Set Extraction AutoInline".
+- Unicode characters in identifiers are now transformed into ascii strings
+  that are legal in Ocaml and other languages.
 - 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.
-- 
cgit v1.2.3