aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-16Merge pull request #203 from CohenCyril/improving_fintype_bigopMaxime Dénès
Improving fintype and bigop
2019-10-16shifting to CHANGELOG_UNRELEASEDCyril Cohen
2019-10-16renaming new `reindex_` lemmas with prefix `big_`Cyril Cohen
2019-10-16Improving fintype and bigopCyril Cohen
### Added - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`. - Bigop theorems: `big_rmcond`, `bigD1_seq`, `reindex_enum_val_cond`, `reindex_enum_rank_cond`, `reindex_enum_val`, `reindex_enum_rank`, `big_set`.
2019-10-15Merge pull request #390 from thery/docCyril Cohen
typo in ssralg
2019-10-14typothery
2019-10-07Merge pull request #384 from pi8027/hierarchyCyril Cohen
Fix and improve the test suite and Makefile
2019-10-07Merge pull request #387 from pi8027/seq-lemmasCyril Cohen
Add `flatten_map1` and `allpairs_consr`
2019-10-05Add flatten_map1 and allpairs_consrKazuhiko Sakaguchi
2019-10-02Fix and improve the test suite and MakefileKazuhiko Sakaguchi
- improve an error message produced by the `check_join` tactic, - fix the build of the test suite: `make test-suite`, and - add a new rule `only` to build a subset of MathComp.
2019-10-01Merge pull request #386 from pi8027/allpairsCyril Cohen
Generalize `allpairs_catr` to non-`eqType`s
2019-09-30Generalize `allpairs_catr` to non-`eqType`sKazuhiko Sakaguchi
2019-09-30Euclid theorem for product (#375)Laurent Théry
2019-09-30ffact as a product similar to fact_prod (#374)Laurent Théry
Thanks!
2019-09-28maxn comment fix (#385)Antonio Nikishaev
2019-09-24Merge pull request #380 from pi8027/ring-core-scopeCyril Cohen
Fix a typo: `ring_core_scope`
2019-09-18Fix a typo: ring_core_scope -> ring_scopeKazuhiko Sakaguchi
2019-09-16fermat little theoremthery
2019-08-12Merge pull request #376 from erikmd/fix-gitlab-yamlCyril Cohen
[ci] fix .gitlab-ci.yml regarding "GIT_STRATEGY: none"
2019-08-10fix(.gitlab-ci.yml): duplicated "variables:" entryErik Martin-Dorel
This could explain why the change in b8eadb8603b83c053a313b39c2a8f268385d8942 was not taken into account.
2019-08-02Merge pull request #373 from erikmd/improve-ciCyril Cohen
[ci] a few improvements of the GitLab CI setup
2019-07-30[ci] Adapt the GitLab CI config to allow scheduled builds for coq-devErik Martin-Dorel
* Normal builds (branches & GitHub PRs) are not impacted * Triggering a scheduled pipeline will only run {coq-dev, mathcomp-dev:coq-dev} to build and deploy the corresponding image to mathcomp/mathcomp-dev:coq-dev. * href: https://docs.gitlab.com/ce/user/project/pipelines/schedules.html
2019-07-30[ci] Add jobs {ci-fourcolor-8.9, ci-odd-order-8.9}Erik Martin-Dorel
* Add {fourcolor, odd-order} test builds with latest Coq release (8.9) * As a result, the math-comp CI config w.r.t. {fourcolor, odd-order} will be similar to that of the upstream repos: - https://github.com/math-comp/fourcolor/blob/master/.travis.yml - https://github.com/math-comp/odd-order/pull/16
2019-07-30refactor: deploy jobs need not clone the repoErik Martin-Dorel
* Set "GIT_STRATEGY: none" accordingly
2019-07-29style: fix indentation detailErik Martin-Dorel
2019-07-11Merge pull request #369 from thery/totientCyril Cohen
totient for prime
2019-07-10totient for primethery
2019-07-05feat(finfun.v): Add tuple_of_finfun, finfun_of_tuple & cancel lemmasCyril Cohen
2019-06-26Merge pull request #364 from erikmd/update/changelogCyril Cohen
docs: Add missing entry in CHANGELOG.md regarding #292
2019-06-26docs: Add missing entry in CHANGELOG.mdErik Martin-Dorel
href: math-comp/math-comp#292
2019-06-18Merge pull request #340 from pi8027/hierarchyEnrico
Reimplement the hierarchy related tools in OCaml
2019-06-11Merge pull request #302 from CohenCyril/fixsetGeorges Gonthier
Fixpoint theorems in finset
2019-06-04Fixpoint theorems in finsetCyril Cohen
2019-05-29Merge pull request #353 from anton-trunov/update-ciCyril Cohen
Remove support for Travis CI (mathcomp switched to Gitlab CI)
2019-05-29Replace eqVneq to destruct both x == y, but also y == x (#351)Cyril Cohen
2019-05-29Remove support for Travis CIAnton Trunov
Mathcomp switched to Gitlab CI via coqbot, see here: https://github.com/math-comp/math-comp/pull/353#issuecomment-497017174
2019-05-29Update pull_request_template.mdCyril Cohen
2019-05-29Merge pull request #352 from CohenCyril/pr_tempateCyril Cohen
PR template
2019-05-29reword entry in CHANGELOG_UNRELEASED.mdAnton Trunov
2019-05-29Update pull_request_template.mdCyril Cohen
2019-05-29Move unreleased changelog entries to CHANGELOG_UNRELEASED.mdAnton Trunov
2019-05-29pr templateCyril Cohen
2019-05-29incorporate new suggestions by @CohenCyrilAnton Trunov
2019-05-29Replace eqVneq with eqPsymAnton Trunov
Also changed eqsVneq.
2019-05-29Canonical way of expressing dis-equality on an eqType is x != yAnton Trunov
Addressing a suggestion by @CohenCyril
2019-05-29Rename eqsP to eqPsym as suggested by @CohenCyrilAnton Trunov
2019-05-28Add eqsP view to destruct not only x == y, but also y == xAnton Trunov
2019-05-22htmldoc regeneratedEnrico Tassi
2019-05-22typoEnrico
2019-05-22Update CHANGELOG.mdGeorges Gonthier
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 18:46:32 +0000