aboutsummaryrefslogtreecommitdiff
path: root/theories/Sorting/PermutEq.v
AgeCommit message (Collapse)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-11-25PermutEq: use “lia” rather than “omega”Vincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib.
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-18List + Permutation : more results about nth_error and nthletouzey
In particular, characterisation of NoDup and Permutation in term of nth_error and nth Some of these results have been suggested last year by Bas Spitters (cf. MathClasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15336 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- 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
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-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
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
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-23Changement de précédence de l'argument du by de assert; ↵herbelin
conséquences sur les .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 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-01-31 18:25:24 +0000