From d13bfeb840d37f93fc60d7141f125f3ff59efc0e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 19 Dec 2001 22:33:59 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index aa3f7d413c..e8e6b51d4e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -16,6 +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
 
 Standard library
 
@@ -30,10 +31,6 @@ Standard library
   properties in plane geometry such as translation, rotation or similarity
   in Rgeom.v; finite sums and Chasles property in Rsigma.v
 
-Efficiency
-
-- Improved efficiency wrt .vo sizes and compilation times
-
 Bugs
 
 - Confusion between implicit args of locals and globals of same base name fixed
-- 
cgit v1.2.3