| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fixing what was presumably a typo in the naming conventions file. |  Hugo Herbelin | 2017-07-16 |
| | | | | | | | | | | Indeed, "forall x, op x x = x" in not in the list, while this is one of the two standard meanings of idempotence. So, knowing that x, y, ... and not n are used elsewhere for variables names, and elt for constants. Moreover, it is probable that before using consistently x, y and z, I had also used m and n, sometimes. So, a convergent probability that it is (just) a typo. | ||
| * | Switch the few remaining iso-latin-1 files to utf8 |  Pierre Letouzey | 2014-12-09 |
| | | |||
| * | Addition of mergesort + cleaning of the Sorting library |  herbelin | 2009-12-13 |
| | | | | | | | | | | | | | | | | | | | | | - 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 | ||
| * | Fixed clash names in Relations (see bug report #2152) and make names | herbelin | 2009-10-08 |
| | | | | | | | | | in Relation_Operators.v and Operators_Properties.v more uniform in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12381 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
| * | Mise à jour du document de révision de la stdlib et déplacement de la | herbelin | 2009-08-14 |
| proposition de nommage standardisé des lemmes dans le trunk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12282 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |