From 674ba52e736691bfb833e588d2687a49e4d146ab Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 23 Jan 2003 00:40:52 +0000
Subject: status de l'extraction

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

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
-- 
cgit v1.2.3