aboutsummaryrefslogtreecommitdiff
path: root/theories/Sorting/PermutSetoid.v
AgeCommit message (Collapse)Author
2009-12-13Addition of mergesort + cleaning of the Sorting libraryherbelin
- 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
2009-10-19Merge SetoidList2 into SetoidList.letouzey
This file contains low-level stuff for FSets/FMaps. Switching it to the new version (the one using Equivalence and so on instead of eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in FSets/FMaps that are minor and probably invisible to standard users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12400 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-04- Add more precise error localisation when one of the application failsherbelin
in a chain of apply or apply-in. - Improved comments on the notions of permutation used in the library (still the equality relation in file Permutation.v misses the property of being effectively an equivalence relation, hence missing expected properties of this notion of permutation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12261 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-19Coq.Relations.Relations can move back to its short nameletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10698 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-14Suppress some warnings by writing ugly Coq.Relations.Relations in some .vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10672 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-06small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is letouzey
more general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10295 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-27eqlistA is now equivlistAletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9913 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-08some more properties of fold and elements in FSetPropertiesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9885 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-16etoffage des notions de permutations (a la fois List.Permutation et ↵letouzey
Permutation.permutation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8823 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 04:24:47 +0000