Les réduction dans les hypothèses s'appliquent maintenant au corps de la définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type

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

1 files changed, 10 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 3b1e5bd1eb..a909449f67 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,13 @@
+Modifications depuis la V7.0
+
+- Fonctions de réduction dans les définitions locales s'appliquent par
+  défaut au corps de la définition. Extension de la notion de Clause
+  pour forcer l'action sur le type des défs seulement sous la forme
+  "Change c in Type of H."
+- Prise en compte des qualid dans Decompose
+- Correction bug inférence type Cases en présence de K-rédex
+- Correction bugs Cases en cas de prédicat dépendant
+
 Différences V7.0beta / V7.0
 - Portage de Correctness
 - Réécriture de Extraction