aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
AgeCommit message (Expand)Author
2020-10-29Switch from long suffixes to short suffixesKazuhiko Sakaguchi
2020-10-12Fixing and documenting the change of meaning of `>=< y`Cyril Cohen
2020-10-12Reorganizing relation between comparability/real and bigCyril Cohen
2020-10-12comparable_big lemma in order.vReynald Affeldt
2020-10-10generalization and shorter proofsCyril Cohen
2020-10-09Added results about `mask` and `subseq`Cyril Cohen
2020-10-07Turn class_of records into primitive records and get rid of the xclass idiomKazuhiko Sakaguchi
2020-09-29ssrnat: add subnA, addnCB, addnCAC, addnAl lemmasAnton Trunov
2020-09-29new mem_imset lemmasChristian Doczkal
2020-09-29rename mem_imset2 to imset2_f (with deprecation)Christian Doczkal
2020-09-29rename mem_imset to imset_f (with deprecation)Christian Doczkal
2020-09-28Submatrix theoryCyril Cohen
2020-09-28Merge pull request #555 from chdoc/disjoint-lemmasCyril Cohen
2020-09-28Apply suggestions from code reviewKazuhiko Sakaguchi
2020-09-27some lemmas for disjointChristian Doczkal
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 12:42:06 +0000