From 794567cd3d35d40b4ad4a4d7a1b0e11e38c4f257 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 6 Oct 2000 16:09:03 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index d0f0012412..6c04f84441 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,9 @@
 - 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é).
+
+- Davantage d'inférence automatique de "?".
 
 - Les cas des Cases ne se lisent plus de manière séquentielle, sauf en
   cas de clauses par défaut redondantes auquel cas la première est prise
@@ -30,4 +33,4 @@ 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"
\ No newline at end of file
+- Ajout (officiel) d'une tactique LetTac et d'un Induction "convivial"
-- 
cgit v1.2.3