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