aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
AgeCommit message (Expand)Author
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
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-05Merge pull request #514 from affeldt-aist/lemmas_from_analysis_20200521Yves Bertot
2020-06-05fix namingReynald Affeldt
2020-06-05Missing mono lemmas (#513)Cyril Cohen
2020-06-04fix namingReynald Affeldt
2020-06-03add real_* variantsReynald Affeldt
2020-06-02another lemma about norm from mathcomp-analysisReynald Affeldt
2020-05-22tentative change of naming convention and add variantsReynald Affeldt
2020-05-21three lemmas that we found useful in the context of theReynald Affeldt
2020-05-16A few more revisionsKazuhiko Sakaguchi
2020-05-13Revise proofs in ssreflect/*.vKazuhiko Sakaguchi
2020-05-04Merge pull request #493 from pi8027/rm-tuple-lemmas-in-orderCyril Cohen
2020-05-04Remove the tuple extensions in order.v that is available in tuple.vKazuhiko Sakaguchi
2020-04-21Add dual_finLatticeType and fix dual_finDistrLatticeTypeKazuhiko Sakaguchi
2020-04-15reworked new lemmas in perm and action and added missing onesCyril Cohen
2020-04-15addressing comments about PR#221 of mathcompReynald Affeldt
2020-04-15Some more lemmas on permutationsFlorent Hivert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:28:57 +0000