From 7221113d52f9bbe7f7a8ee1452f97116d0b260df Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 23 Mar 2001 23:50:08 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index e5001aaf47..bc61c4b8b8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,8 @@ Diff
    - Rel not in scope of ?
    - implicits in inductive defs
    - localisation des erreurs avec Syntactif Definition
+   - clauses par défaut de Cases non lues séquentiellement
+   - plusieurs bugs avec les prédicats de Cases lorsque dépendants
 - 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
@@ -13,6 +15,7 @@ Diff
 - Possibilité de déplier des définitions locales à un but
 - Suppression message .coqrc
 - Add ML Path est fait automatiquement par Add LoadPath
+- Nouveau mécanisme de nommage des schémas d'élimination (incompatibilités...)
 
 Différences oubliées dans la V7.0beta :
 
-- 
cgit v1.2.3