aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-09-30ffact as a product similar to fact_prod (#374)Laurent Théry
2019-09-28maxn comment fix (#385)Antonio Nikishaev
2019-09-24Merge pull request #380 from pi8027/ring-core-scopeCyril Cohen
2019-09-18Fix a typo: ring_core_scope -> ring_scopeKazuhiko Sakaguchi
2019-09-16fermat little theoremthery
2019-09-05Redirects to math-comp.github.ioCyril Cohen
2019-08-12Merge pull request #376 from erikmd/fix-gitlab-yamlCyril Cohen
2019-08-10fix(.gitlab-ci.yml): duplicated "variables:" entryErik Martin-Dorel
2019-08-02Merge pull request #373 from erikmd/improve-ciCyril Cohen
2019-07-30[ci] Adapt the GitLab CI config to allow scheduled builds for coq-devErik Martin-Dorel
2019-07-30[ci] Add jobs {ci-fourcolor-8.9, ci-odd-order-8.9}Erik Martin-Dorel
2019-07-30refactor: deploy jobs need not clone the repoErik Martin-Dorel
2019-07-29style: fix indentation detailErik Martin-Dorel
2019-07-11Merge pull request #369 from thery/totientCyril Cohen
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
2019-06-26docs: Add missing entry in CHANGELOG.mdErik Martin-Dorel
2019-06-18Merge pull request #340 from pi8027/hierarchyEnrico
2019-06-11Merge pull request #302 from CohenCyril/fixsetGeorges Gonthier
2019-06-04Fixpoint theorems in finsetCyril Cohen
2019-05-29Merge pull request #353 from anton-trunov/update-ciCyril Cohen
2019-05-29Replace eqVneq to destruct both x == y, but also y == x (#351)Cyril Cohen
2019-05-29Remove support for Travis CIAnton Trunov
2019-05-29Update pull_request_template.mdCyril Cohen
2019-05-29Merge pull request #352 from CohenCyril/pr_tempateCyril Cohen
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
2019-05-29Canonical way of expressing dis-equality on an eqType is x != yAnton Trunov
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
2019-05-22Update INSTALL.mdEnrico
2019-05-22be explicit about opam version 2.xEnrico
2019-05-22Update README.mdCyril Cohen
2019-05-21Update CHANGELOG.mdCyril Cohen
2019-05-17Merge pull request #345 from math-comp/perm-tallyGeorges Gonthier
2019-05-17refactor `seq` permutation theoryGeorges Gonthier
2019-05-08Merge pull request #344 from soraros/ssrnat-remove-arith-lemmasGeorges Gonthier
2019-05-08suppress use of `Arith` hintsSora Chen
2019-05-06Merge pull request #342 from math-comp/deprecationGeorges Gonthier
2019-05-06add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma namesGeorges Gonthier
2019-04-30Ad-hoc fixKazuhiko Sakaguchi
2019-04-30Reimplement the hierarchy related tools in OCamlKazuhiko Sakaguchi