maj CHANGES extraction + bug extraction & _

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2359 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 623ded3ea..d978702e9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,15 @@ Tactics
 - Slight improvement in naming strategy for NewInduction/NewDestruct
 - Intuition/Tauto do not perform useless unfolding and work up to conversion
 
+Extraction
+
+See contrib/extraction/CHANGES or documentation. In brief: 
+- Syntax changes: there are no more options inside the extraction commands. 
+  New commands for customization and options have been introduced instead. 
+- More optimizations on extracted code. 
+- Extraction tests are now embbeded in 14 user contributions. 
+
+
 Standard library
 
 - In [Relations], Rstar.v and Newman.v now axiom-free.