aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-08-11fix notation-incompatible-format warningsChristian Doczkal
2020-08-11Merge pull request #507 from pi8027/test-guard-condCyril Cohen
Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition
2020-08-11Merge pull request #542 from chdoc/nothing-to-injectCyril Cohen
fix "Nothing to inject" warnings
2020-08-11Merge pull request #551 from CohenCyril/merge-changelog-by-unionCyril Cohen
Use union driver for CHANGELOG_UNRELEASED
2020-08-11Use union driver for CHANGELOG_UNRELEASEDCyril Cohen
2020-08-11Merge pull request #541 from chdoc/properCCyril Cohen
lemmas for proper and setC
2020-08-11Merge pull request #536 from pi8027/hierarchyCyril Cohen
Fix some hierarchy.ml related issues
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
- pass `Unix.environment ()` to `coqtop` to preserve the parent process environment, - check the exit status of `coqtop` and report an error if it is wrong, - do not rely on `ssrfun.id` in the `check_join` tactic, and - improve the error message for missing unification hints.
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
fix the doc for ubnP in ssrnat
2020-06-24Merge pull request #539 from thery/sum_nat_constCyril Cohen
simpler proof of sum_nat_const_nat in bigop.v
2020-06-24missing bigop lemmas (#537)Laurent Théry
* missing lemmas discovered while developing mathcomp-analysis Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr> * Intermediate lemmas and shortening proofs (thanks Laurent) Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr> Co-authored-by: Cyril Cohen <cohen@crans.org>
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
Card lemmas
2020-06-18conform to 80 chars limitChristian Doczkal
2020-06-18fixup spacingCyril Cohen
2020-06-18Apply suggestions from code reviewChristian Doczkal
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
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
contra lemmas involving propositions
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
guard condition
2020-06-10Merge pull request #535 from CohenCyril/allow-coq-devCyril Cohen
Generated opam packages allow coq-dev again
2020-06-10Generated opam packages allow coq-dev againCyril Cohen
As a result of [a discussion on Zulip](https://coq.zulipchat.com/#narrow/stream/237665-math-comp-devs/topic/MathComp.201.2E11.2E0.20OPAM.20packages.20Coq.20compatibility) Reverts "removing opam `| (= "dev")` for released packages" (commit 313e44316177c918b363c118f15297e08d13eb4e).
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
edit changelogs before release
2020-06-09Merge pull request #534 from CohenCyril/doc-1.11Cyril Cohen
add lua&sed to nixshell and switch to coq 8.11 + fixing doc
2020-06-09add lua&sed to shell and switch to coq 8.11 + fixing docCyril Cohen
2020-06-09edit changelogs before releaseReynald Affeldt
2020-06-09Merge pull request #532 from CohenCyril/silence-8.12-warningsCyril Cohen
fix coq 8.12 warnings
2020-06-09fix coq 8.12 warningsCyril Cohen
2020-06-08Merge pull request #531 from CohenCyril/fix_cyclotomicCyril Cohen
turning let into local definition
2020-06-08turning let into local definitionCyril Cohen
2020-06-08Merge pull request #528 from CohenCyril/silence_warningsCyril Cohen
silencing warnings in individual packages
2020-06-08silencing warnings in individual packagesCyril Cohen
2020-06-08Merge pull request #519 from CohenCyril/homomono_inYves Bertot
Missing homo/mono lemmas in the presence of cancellation
2020-06-08Cachix action (#525)Cyril Cohen
tentative fix
2020-06-08Documenting addition policy to coq.Cyril Cohen
2020-06-08Merge pull request #524 from erikmd/coq-8.12Cyril Cohen
[CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha)
2020-06-07[CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha)Erik Martin-Dorel
2020-06-06Merge pull request #522 from affeldt-aist/update_readmeCyril Cohen
change links to the wiki to links to the website
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 14:48:24 +0000