From b12216126dbe75d179ad2a66b866e0e0c93e69bc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 20 Dec 2000 19:51:08 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index d8d9f0e1b9..8744effdb7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -134,10 +134,8 @@ Tactiques
   - Correction de bugs (quand le type ne commence pas par un inductif)
     et refus d'agir sous les ->.
 
-- 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é.
+- Simpl ne déplie plus les appels récursifs d'un Fix mutuel réduit. 
+  Rem: c'est une source d'incompatibilité.
 
 - Intro échoue si le nom d'hypothèse existe au lieu de mettre un avertissement
 
@@ -148,8 +146,9 @@ Tactiques
 - AutoRewrite ne s'occupe maintenant que du but principal et c'est les
   Hint Rewrite qui gèrent les sous-buts générés
 
-- Redondant or incompatible instantiations in Apply ... with now
-  correctly trapped
+- Les instantiations redondantes ou incompatibles de Apply ... with ...
+  sont maintenant correctement traitées.
+
 
 Outils
 
-- 
cgit v1.2.3