changements de dernieres minutes pour la 8.1 beta:

- qualification correcte des noms en Haskell
- on imprime les types de toutes les fonctions en Haskell
- en Ocaml, les appels recursifs d'une f : 'a truc doivent 
 se faire avec les _meme_ parametres de types 'a. Exemple illegal: 
   let rec f = function [] -> 0 | l -> f [l];;
 On met maintenant des Obj.magic en conséquence. 
 En Haskell (avec typage fourni), ca passe. 



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

1 files changed, 6 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index f6e75bfd37..f2d672233c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -98,9 +98,12 @@ Tactics
 
 Extraction
  
-- all type parts should now disappear instead of sometimes producing _ 
+- All type parts should now disappear instead of sometimes producing _ 
   (for instance in Map.empty).
-- TODO bug fixes...
+- Haskell extraction: types of functions are now printed, better 
+  unsafeCoerce mechanism, both for hugs and ghc
+- Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme
+- Many bug fixes
 
 Modules
 
@@ -124,7 +127,7 @@ Notations
 Libraries
 
 - New library on String and Ascii characters (contributed by L. Thery)
-- New library FSets+FMaps of finite sets and maps (TODO doc quelque part)
+- New library FSets+FMaps of finite sets and maps (TODO doc)
 - New library QArith on rational numbers
 - Small extension of Zmin.V, new Zmax.v, new Zminmax.v
 - Reworking of the files on classical logic and description principles