documentation de mes actions recentes sur les theories (PL)

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

1 files changed, 22 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index c6d4d21bb..639550e94 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,25 @@
+Changes from V7.1 to V7.2
+========================
+
+Standard library
+----------------
+
+- In [Relations], the files Rstar.v and Newman.v are now axiom-free. 
+
+- In [Sets], the file Integers.v uses directly the type nat and 
+   not any more an encapsulation Nat. Consequent simplifications. 
+
+- In [Arith], the file Min.v contains now more lemmas, and a dual file 
+   Max.v has been introduced. 
+
+- In [Arith], a tail-recursive plus and mult are now defined. Cf. files 
+   Plus.v and Mult.v	
+
+- 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
 ========================