From c51c32b09cbdad951c55c7f7dd5f47b6657d32a8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 20 Dec 2001 22:48:06 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index e8e6b51d4e..623ded3eae 100644
--- a/CHANGES
+++ b/CHANGES
@@ -16,7 +16,7 @@ Tactics
 - New tactic "ClearBody H" to clear the body of definitions in local context
 - New tactic "Assert H := c" for forward reasoning
 - Slight improvement in naming strategy for NewInduction/NewDestruct
-- Intuition/Tauto does not perform useless unfolding
+- Intuition/Tauto do not perform useless unfolding and work up to conversion
 
 Standard library
 
@@ -56,6 +56,7 @@ Incompatibilities
 - Extra parentheses may exceptionally be needed in tactic definitions.
 - Coq extensions written in Ocaml need to be updated (see dev/changements.txt
   for a description of the main changes in the interface files of V7.2)
+- New behaviour of Intuition/Tauto may exceptionally lead to incompatibilities
 
 ----------------------------------------------------------------------------
 Changes from V6.3.1 and V7.0 to V7.1
-- 
cgit v1.2.3