From e595bdc0a43cd057cb403b2e1cac125135780549 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 31 Jan 2001 21:42:44 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index 3b2dcacd4d..c16edc11ae 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
-- 
cgit v1.2.3