MAJ

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

1 files changed, 1 insertions, 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