From 8ed67d4a2dabe40186c8ad0550fb3fbd2d9b8787 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Jun 2001 13:37:10 +0000
Subject: 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
---
 CHANGES | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'CHANGES')

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
-- 
cgit v1.2.3