aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-26Update pull_request_template.mdCyril Cohen
2020-08-20Merge pull request #550 from jashug/dont-refresh-argument-names-overlayEnrico Tassi
2020-08-17Merge pull request #547 from pi8027/qualified-dual-opCyril 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-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-13Merge pull request #494 from pi8027/rm-displays-in-classesCyril 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-11Merge pull request #552 from chdoc/rel-format-warningCyril Cohen
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 #551 from CohenCyril/merge-changelog-by-unionCyril Cohen
2020-08-11Use union driver for CHANGELOG_UNRELEASEDCyril Cohen
2020-08-11Merge pull request #541 from chdoc/properCCyril Cohen
2020-08-11Merge pull request #536 from pi8027/hierarchyCyril Cohen
2020-06-27Fix some Makefile issues and rename `hierarchy_test.v` to `test_hierarchy_all.v`Kazuhiko Sakaguchi
2020-06-27Fix bugs in hierarchy.mlKazuhiko 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 bigop lemmas (#537)Laurent Théry
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-19Merge pull request #509 from chdoc/card-lemmasCyril Cohen
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-17Merge pull request #499 from chdoc/contra-propCyril Cohen
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-10Merge pull request #535 from CohenCyril/allow-coq-devCyril Cohen
2020-06-10Generated opam packages allow coq-dev againCyril Cohen
2020-06-09removing opam `| (= "dev")` for released packagesCyril Cohen
2020-06-09Complying to SPDXCyril Cohen
2020-06-09fixing mailmapCyril Cohen
2020-06-09mailmap for Yves and ReynaldCyril Cohen
2020-06-09Merge pull request #533 from affeldt-aist/changelogs_before_releaseaffeldt-aist
2020-06-09Merge pull request #534 from CohenCyril/doc-1.11Cyril Cohen