aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
AgeCommit message (Expand)Author
2020-09-27Putting ord1 in fintypeCyril Cohen
2020-09-17Fix big meet and join notations for dual_display, and add `0^d` and `1^d` not...Kazuhiko Sakaguchi
2020-09-16add missing contra lemmas (fixes #587)Christian Doczkal
2020-09-10Merge pull request #492 from CohenCyril/big_rmcondKazuhiko Sakaguchi
2020-09-10Merge pull request #578 from CohenCyril/contra_leKazuhiko Sakaguchi
2020-09-08split_find_nth and split_find lemmasCyril Cohen
2020-09-05Adding contra lemmas with ordersCyril Cohen
2020-09-03compat Coq < 8.10Cyril Cohen
2020-09-03Lemmas reindex_omap and bigD1_ordCyril Cohen
2020-09-03Merge pull request #558 from CohenCyril/are_allpairsEnrico Tassi
2020-09-03Adding allrel predicateCyril Cohen
2020-09-03New `big_uncond` and `big_rmcond -> big_rmcond_in`Cyril Cohen
2020-09-03Expliciting relation between split and [lr]shiftCyril Cohen
2020-09-01fix for Coq 8.7Cyril Cohen
2020-09-01Adding sig_big_dep lemmaCyril Cohen
2020-08-25Adding lemma `oddS`Cyril Cohen
2020-08-17Qualify the dual_* notations with the Order moduleKazuhiko Sakaguchi
2020-08-16Merge pull request #517 from thery/minnCyril Cohen
2020-08-15Extra theorems about subn min and maxthery
2020-08-13Merge pull request #553 from chdoc/non-reversible-notationCyril Cohen
2020-08-13fix non-reversible-notation warningsChristian Doczkal
2020-08-12Get rid of displays in class fields and mixin parametersKazuhiko Sakaguchi
2020-08-11fix notation-incompatible-format warningsChristian Doczkal
2020-08-11Merge pull request #542 from chdoc/nothing-to-injectCyril Cohen
2020-06-26fix "Nothing to inject" warningsChristian Doczkal
2020-06-26lemmas for proper and setCChristian Doczkal
2020-06-24Merge pull request #540 from thery/docCyril Cohen
2020-06-24fix the doc for ubnP in ssrnatthery
2020-06-24simpler proofthery
2020-06-18conform to 80 chars limitChristian Doczkal
2020-06-18fixup spacingCyril Cohen
2020-06-18Apply suggestions from code reviewChristian Doczkal
2020-06-18drop_uniq / CHANGELOGChristian Doczkal
2020-06-18add fcard_gt?P lemmas found in fourcolorChristian Doczkal
2020-06-18cards_eqP and cards2PChristian Doczkal
2020-06-18cardinality lemmas for #|A| <= 1 and n <= #|A|Christian Doczkal
2020-06-17contra lemmas involving propositionsChristian Doczkal
2020-06-09add lua&sed to shell and switch to coq 8.11 + fixing docCyril Cohen
2020-06-09fix coq 8.12 warningsCyril Cohen
2020-06-08Merge pull request #528 from CohenCyril/silence_warningsCyril Cohen
2020-06-08silencing warnings in individual packagesCyril Cohen
2020-06-08Documenting addition policy to coq.Cyril Cohen
2020-06-06bugfixCyril Cohen
2020-06-06Missing homo_mono lemmasCyril Cohen
2020-06-06ImprovementsCyril Cohen
2020-06-06tentative changelogReynald Affeldt
2020-06-06General theory of min and max, and use in ssrnumCyril Cohen
2020-06-06Increasing definitional equalitiesCyril Cohen
2020-06-06Generalizing max and min to porderTypeCyril Cohen
2020-06-05Missing mono lemmas (#513)Cyril Cohen
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 19:44:40 +0000