changements récents dans l'extraction

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

1 files changed, 5 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 2cd576a702..5b75441115 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,11 @@ Bugs
 - "Intros H" now working like "Intro H" trying first to reduce if not a product
 - Forward dependencies in Cases now taken into account
 
+Extraction (details in contrib/extraction/CHANGES or documentation)
+
+- Signatures of extracted terms are now mostly expunged from dummy arguments. 	
+- Haskell extraction is now operational (tested & debugged).  
+
 Standard library
 
 - Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v and Zlogarithms.v)