| Age | Commit message (Expand) | Author |
| 2019-12-11 | Add (meet|join)_(l|r), some renamings, and small cleanups | Kazuhiko Sakaguchi |
| 2019-12-11 | Fixes in naming, mixins, doc and canonical ordering | Cyril Cohen |
| 2019-12-11 | Make an appropriate use of the order library everywhere (#278, #280, #282, #2... | Kazuhiko Sakaguchi |
| 2019-11-29 | update changelogs for the 1.10.0 release | Yves Bertot |
| 2019-11-29 | Return of PR #226: adds relevant theorems when fcycle f (orbit f x) and the n... | Cyril Cohen |
| 2019-11-28 | Merge pull request #439 from math-comp/CohenCyril-patch-1 | Cyril Cohen |
| 2019-11-27 | Explicit `bigop` enumeration handling | Georges Gonthier |
| 2019-11-25 | remove duplicated sentence in CHANGELOG_UNRELEASED | Cyril Cohen |
| 2019-11-22 | Injectivity lemmas in fintype (#426) | Kazuhiko Sakaguchi |
| 2019-11-22 | Added ssrfun theorem `inj_compr` (#432) | Cyril Cohen |
| 2019-11-22 | New generalised induction idiom (#434) | Georges Gonthier |
| 2019-11-20 | Merge pull request #399 from CohenCyril/ltn_sub | Yves Bertot |
| 2019-11-19 | Merge pull request #420 from pi8027/all-lemmas | Cyril Cohen |
| 2019-11-18 | fixing CHANGELOG and ltn_pred lemmas | Cyril Cohen |
| 2019-11-18 | More arithmetic theorems | Cyril Cohen |
| 2019-11-15 | More lemmas on seqs | Florent Hivert |
| 2019-11-15 | Add all_filter, all_pmap, and all_allpairsP in seq.v | Kazuhiko Sakaguchi |
| 2019-11-14 | fingraph: remove fin_inj_bij lemma as duplicate of injF_bij from fintype (#403) | Anton Trunov |
| 2019-11-14 | Lemmas on commutation with big sum and prod (#413) | Florent Hivert |
| 2019-11-06 | Merge pull request #408 from chdoc/existsPn | Cyril Cohen |
| 2019-11-06 | Merge pull request #406 from hivert/algebras | Cyril Cohen |
| 2019-11-04 | add existsPn/forallPn lemmas | Christian Doczkal |
| 2019-11-03 | Interface for commutative and commutative-unitary algebras | Florent Hivert |
| 2019-10-30 | Change the order of arguments in `ltngtP` | Kazuhiko Sakaguchi |
| 2019-10-25 | Removing duplicate lemma `addnKC` (= `addKn`) | Cyril Cohen |
| 2019-10-25 | Merge pull request #396 from CohenCyril/edivnD | Laurent Théry |
| 2019-10-25 | Instances for empty type. (#393) | Arthur Azevedo de Amorim |
| 2019-10-25 | Stability proofs of sort (#358) | Kazuhiko Sakaguchi |
| 2019-10-25 | More arithmetic theorems | Cyril Cohen |
| 2019-10-24 | Added and generalized arithmetic theorems. (#394) | Cyril Cohen |
| 2019-10-16 | shifting to CHANGELOG_UNRELEASED | Cyril Cohen |
| 2019-10-07 | Merge pull request #384 from pi8027/hierarchy | Cyril Cohen |
| 2019-10-05 | Add flatten_map1 and allpairs_consr | Kazuhiko Sakaguchi |
| 2019-10-02 | Fix and improve the test suite and Makefile | Kazuhiko Sakaguchi |
| 2019-09-30 | Generalize `allpairs_catr` to non-`eqType`s | Kazuhiko Sakaguchi |
| 2019-09-30 | Euclid theorem for product (#375) | Laurent Théry |
| 2019-09-30 | ffact as a product similar to fact_prod (#374) | Laurent Théry |
| 2019-09-16 | fermat little theorem | thery |
| 2019-07-10 | totient for prime | thery |
| 2019-07-05 | feat(finfun.v): Add tuple_of_finfun, finfun_of_tuple & cancel lemmas | Cyril Cohen |
| 2019-06-04 | Fixpoint theorems in finset | Cyril Cohen |
| 2019-05-29 | reword entry in CHANGELOG_UNRELEASED.md | Anton Trunov |
| 2019-05-29 | Move unreleased changelog entries to CHANGELOG_UNRELEASED.md | Anton Trunov |