From 37920925cd660cf172bb49bb9b1b37999fa33221 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 21 Nov 2001 15:08:06 +0000
Subject: 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
---
 CHANGES | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/CHANGES b/CHANGES
index c6d4d21bbb..639550e94f 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
 ========================
 
-- 
cgit v1.2.3