From 49710f8dc330af5b1db10d1158d990dce330d224 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 15 Mar 2002 13:52:58 +0000
Subject: changements récents dans l'extraction

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

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