From a7b8e9c4e5c0e915cc8d16e9b673e7a0a280e1fe Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Sep 2001 14:57:19 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index a1d55209aa..8811c651f0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -32,6 +32,12 @@ Diff
 - 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
 - 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
-- 
cgit v1.2.3