MAJ

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

1 files changed, 6 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 6c04f8444..08802e053 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,8 +7,10 @@
 - Numérotation dans l'ordre des hypothèses créées par Decompose
 - Correction de bugs (quand le type ne commence pas par un inductif)
 
-- Simpl ne déplie plus les appels récursifs d'un Fix mutuel réduit
-  Il réduit un peu plus aussi (source d'incompatibilité).
+- Simpl ne déplie plus les appels récursifs d'un Fix mutuel réduit. En
+revanche, si une constante n'est qu'indirectement un Fix, on ne garde
+en général plus son nom (sauf dans les cas "simples"). Rem : c'est une
+source d'incompatibilité.
 
 - Davantage d'inférence automatique de "?".
 
@@ -34,3 +36,5 @@ l'ast, il faut typer explicitement la grammaire avec Ast ou List
 - Ajout d'un Let primitif
 
 - Ajout (officiel) d'une tactique LetTac et d'un Induction "convivial"
+
+- Langage de tactique