MAJ

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

1 files changed, 7 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index a1d55209aa..8811c651f0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -32,6 +32,12 @@ Différences oubliées dans la V7.0beta :
 - les objets non persistants (Grammaires, Hints) d'un module chargé par Require
 disparaissent à la fermeture de la section si le Require est dans la
 section. Les Require ultérieurs ne les réintroduisent pas.
+- Un lieur multiple comme (a:A)(a,b,c:(P a))(Q a), n'est plus compris comme
+  (a:A)(a0:(P a))(b:(P a),c:(P a))(Q a0), mais comme 
+  (a:A)(a0:(P a))(b:(P a0),c:(P a0))(Q a0)
+- Les noms de variables des projections de Record sont maintenant basés sur
+  l'initiale de leur type.
+
 
 Différences V7.0beta / V7.0
 
@@ -60,7 +66,7 @@ Différences oubliées dans la V7.0beta :
 - Du fait des noms qualifiés, les variables de buts n'évitent plus les
   globaux de même nom de base
 - Unfold ne peut s'appliquer qu'à des constantes dépliables (en
-  particulier pas à des Syntactic Definition)
+  particulier pas à des Syntactic Definition, ni des types inductifs)
 
 ----------------------------------------------------------------------
 English version of changes is available on