status de l'extraction

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

1 files changed, 8 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 040f050c80..5c1ef12a91 100644
--- a/CHANGES
+++ b/CHANGES
@@ -104,6 +104,14 @@ Tactics
 - Unfold expects a correct evaluable argument
 - Clear expects existing hypotheses
 
+Extraction (See details in contrib/extraction/CHANGES and README):
+
+- An experimental Scheme extraction is provided.
+- Concerning Ocaml, extracted code is now ensured to always type-check, 
+  thanks to automatic inserting of Obj.magic.
+- "early" (read: "still bugged") version of an extraction compatible with
+  Coq's new modules.
+
 Miscellaneous
 
 - Printing Coercion now used through the standard keywords Set/Add, Test, Print