aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/seq.v
AgeCommit message (Expand)Author
2021-03-07Adding Order.enum and related definitions and theoremsCyril Cohen
2021-01-22Remove deprecation aliases introduced in 1.9.0Kazuhiko Sakaguchi
2021-01-16Drop support for Coq 8.10 and deprecate the `deprecate` notationKazuhiko Sakaguchi
2020-12-16Add `pairwise r xs` predicateKazuhiko Sakaguchi
2020-11-25Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entriesKazuhiko Sakaguchi
2020-11-25Apply suggestions from code reviewKazuhiko Sakaguchi
2020-11-25Apply suggestions from code reviewKazuhiko Sakaguchi
2020-11-25Generalize `allrel` to take two lists as argumentsKazuhiko Sakaguchi
2020-11-24Add more `_in` lemmas and CHANGELOG entriesKazuhiko Sakaguchi
2020-11-24factoring out in_sigCyril Cohen
2020-11-24Add `_in` lemmas for `sort`Kazuhiko Sakaguchi
2020-11-23Merge pull request #667 from CohenCyril/ssrcoq8.10Enrico Tassi
2020-11-20Tuning simplifications using Arguments simpl nomatchCyril Cohen
2020-11-20Using Coq 8.10 ssreflect new featuresCyril Cohen
2020-11-20typo in documentation of allpairs_depYves Bertot
2020-11-19add declare scopesReynald Affeldt
2020-11-12Apply suggestions from KazuhikoCyril Cohen
2020-11-12Equivalences instead of implications for `count_maskP` and `count_subseqP`Cyril Cohen
2020-11-12Shorter proofs and suggestions by KazuhikoCyril Cohen
2020-11-12Adding some theory for `rem` and generalizing `subset_maskP`Cyril Cohen
2020-11-11Merge pull request #640 from CohenCyril/fix_iota_addCyril Cohen
2020-11-11make pivot the first argument in uniq_subseq_pivotChristian Doczkal
2020-11-11turn uniq_subseq_pivot into equalityChristian Doczkal
2020-11-11Apply suggestions from code reviewChristian Doczkal
2020-11-11fixup after feedback from CyrilChristian Doczkal
2020-11-11Apply suggestions from code reviewChristian Doczkal
2020-11-11suggestions from CyrilChristian Doczkal
2020-11-11lemmas on subseq and rotChristian Doczkal
2020-11-11Deprecation of iota_add delayed, and not the one of iter_addCyril Cohen
2020-11-11Merge pull request #632 from pi8027/path-cycle-sortedCyril Cohen
2020-11-11New lemmas about allpairsCyril Cohen
2020-11-11Apply suggestions from code reviewKazuhiko Sakaguchi
2020-11-10Reorganize, generalize, and add lemmas about `path`, `cycle`, and `sorted`Kazuhiko Sakaguchi
2020-11-02lemmas for reasoing about "rot n (rot m s)"Christian Doczkal
2020-10-29Switch from long suffixes to short suffixesKazuhiko Sakaguchi
2020-10-10generalization and shorter proofsCyril Cohen
2020-10-09Added results about `mask` and `subseq`Cyril Cohen
2020-09-08split_find_nth and split_find lemmasCyril Cohen
2020-09-03Adding allrel predicateCyril Cohen
2020-06-18drop_uniq / CHANGELOGChristian Doczkal
2020-06-18cardinality lemmas for #|A| <= 1 and n <= #|A|Christian Doczkal
2020-05-16A few more revisionsKazuhiko Sakaguchi
2020-05-13Revise proofs in ssreflect/*.vKazuhiko Sakaguchi
2020-04-10Make `all2` better wrt the guard conditionCyril Cohen
2020-04-09- switching long suffixes to short suffixesReynald Affeldt
2020-04-02Merge pull request #468 from ybertot/remove-deprecated-from-1.9Enrico Tassi
2020-04-01Merge pull request #429 from pi8027/extend-nat-comparisonYves Bertot
2020-03-31remove deprecated commands whose deprecation was introduced in release 1.9.0Yves Bertot
2020-03-15Extend comparison predicates for nat with minn and maxnKazuhiko Sakaguchi
2020-01-28Added lemmas about foldl, scanl, foldr and rcons and consCyril Cohen
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:53:38 +0000