| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
this fixes #2441 (even though some other problem was involved too that
r16673 might have solved).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13677 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12772 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
- 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
|
herbelin
letouzey