From f698148f6aee01a207ce5ddd4bebf19da2108bff Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 13 Dec 2009 21:23:17 +0000
Subject: Addition of mergesort + cleaning of the Sorting library - New
 (modular) mergesort purely using structural recursion - Move of the (complex)
 notion of permutation up to setoid equality   formerly defined in
 Permutation.v to file PermutSetoid.v - Re-use of the file Permutation.v for
 making the canonical notion   of permutation that was in List.v more visible
 - New file Sorted.v that contains two definitions of sorted:   "Sorted" is a
 renaming of "sort" that was defined in file   Sorting.v and "StronglySorted"
 is the intuitive notion of sorted   (there is also LocallySorted which is a
 variant of Sorted) - File Sorting.v is replaced by a call to the main Require
 of the directory - The merge function whose specification rely on counting
 elements is moved   to Heap.v and both are stamped deprecated (the sort
 defined in   Heap.v has complexity n^2 in worst case) - Added some new naming
 conventions - Removed uselessly-maximal implicit arguments of Forall2
 predicate

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12585 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 686b226ed7..9998364d9f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -121,7 +121,16 @@ Library
   available under the name nat_compare_alt.
 - Lemmas in library Relations and Reals have been homogenized a bit.
 - The implicit argument of Logic.eq is now maximally inserted, allowing
-  to simply write "eq" instead of "@eq _" in morphism signatures. 
+  to simply write "eq" instead of "@eq _" in morphism signatures.
+- Revision of the Sorting library:
+  - new mergesort of worst-case complexity O(n*ln(n)) made available in 
+    Mergesort.v;
+  - notion of permutation up to setoid from Permutation.v is deprecated and 
+    was moved to PermutSetoid.v;
+  - Permutation.v now contains the notion of permutation that was formerly in 
+    List.v;
+  - heapsort from Heap.v of worst-case complexity O(n*n) is deprecated;
+  - new file Sorted.v for some definitions of being sorted.
 
 Changes from V8.1 to V8.2
 =========================
-- 
cgit v1.2.3