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

1 files changed, 10 insertions, 1 deletions

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
 =========================