From e58d53c629a47d36cb58edf33cd5e3b5cbec17fd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Oct 2000 22:56:46 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index 6c04f84441..08802e0533 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
-- 
cgit v1.2.3