MAJ

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

1 files changed, 7 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 3b2dcacd4..c16edc11a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,13 +1,18 @@
 Différences V7.0beta / V7.0
 
 - Ajout de déclarations locales aux Record (record à la Randy).
-- Correction de bugs (Identity Coercion; Rel not in scope of ?;
-  implicits in inductive defs).
+- Correction de bugs
+   - Identity Coercion
+   - Rel not in scope of ?
+   - implicits in inductive defs
+   - localisation des erreurs avec Syntactif Definition
 - Prise en compte noms longs dans Hints, Coercions et Unfold
 - Rétablissement des @Definition and co
 - Rétablissement des token extensibles et mélangeant symboles et lettres
+- Ajout d'une option Set/Unset/Test Printing Coercions
 - Possibilité de déplier des définitions locales à un but
 
+
 Différences oubliées dans la V7.0beta :
 
 - Du fait des noms qualifiés, les variables de buts n'évitent plus les