MAJ

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

1 files changed, 14 insertions, 18 deletions

diff --git a/CHANGES b/CHANGES
index 4266e0e9b3..e268f14c81 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,20 @@
 Changes from V7.1 to V7.2
 ========================
 
+Language
+
+- Automatic insertion of patterns for local definitions in the type of
+  the constructors of an inductive types (for compatibility with V6.3
+  let-in style)
+- Coercions allowed in Cases patterns
+
+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 (may
+  occasionnally affect compatibility with V7.1 NewInduction/NewDestruct)
+
 Standard library
 ----------------
 
@@ -18,24 +32,6 @@ Standard library
 - A new directory named [Sorting] contains a proof of a heapsort. 
    (theory forgotten during the port of V6.3 to V7.0) 
 
-
-----------------------------------------------------------------------------
-Changes from ??? to V7.1
-========================
-
-Language
-
-- Automatic insertion of patterns for local definitions in the type of
-  the constructors of an inductive types (for compatibility with V6.3
-  let-in style)
-
-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 (may
-  occasionnally affect compatibility with V7.1 NewInduction/NewDestruct)
-
 Efficiency
 
 - Improved efficiency wrt .vo sizes and compilation times