aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
AgeCommit message (Expand)Author
2020-09-03Lemmas mxminpoly_minP and dvd_mxminpolyCyril Cohen
2020-09-03Merge pull request #558 from CohenCyril/are_allpairsEnrico Tassi
2020-09-03Merge pull request #565 from CohenCyril/split_ordPLaurent Théry
2020-09-03Merge pull request #564 from CohenCyril/pinvmxLaurent Théry
2020-09-03Adding allrel predicateCyril Cohen
2020-09-03Merge pull request #560 from CohenCyril/commr_hornerLaurent Théry
2020-09-03More pinvmx theoryCyril Cohen
2020-09-03Adding commr_horner lemmaCyril Cohen
2020-09-03Expliciting relation between split and [lr]shiftCyril Cohen
2020-09-03Extracting a nonzero coefficient from a nonzero matrixCyril Cohen
2020-09-03Elementary theory of diagonal and triagular matricesCyril 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-20Merge pull request #550 from jashug/dont-refresh-argument-names-overlayEnrico Tassi
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-13Be robust to a change in the default argument naming algorithm.Jasper Hugunin
2020-08-13Merge pull request #545 from pi8027/fieldextCyril Cohen
2020-08-13Merge pull request #553 from chdoc/non-reversible-notationCyril Cohen
2020-08-13fix non-reversible-notation warningsChristian Doczkal
2020-08-12Make [fieldExtType F of L] work for abstract instancesKazuhiko Sakaguchi
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 #507 from pi8027/test-guard-condCyril Cohen
2020-08-11Merge pull request #542 from chdoc/nothing-to-injectCyril Cohen
2020-08-11Merge pull request #541 from chdoc/properCCyril Cohen
2020-06-27Fix some Makefile issues and rename `hierarchy_test.v` to `test_hierarchy_all.v`Kazuhiko Sakaguchi
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-24Merge pull request #539 from thery/sum_nat_constCyril Cohen
2020-06-24missing lemmas discovered while developing mathcomp-analysisReynald Affeldt
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-13Add more test cases for higher-order recursive functions in seq.v w.r.t. the ...Kazuhiko Sakaguchi
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-08turning let into local definitionCyril Cohen
2020-06-08Merge pull request #528 from CohenCyril/silence_warningsCyril Cohen
2020-06-08silencing warnings in individual packagesCyril Cohen
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:43:00 +0000