index
:
coq-mathcomp
master
Library of mathematical components formalized in Coq
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-09-30
ffact as a product similar to fact_prod (#374)
Laurent Théry
2019-09-28
maxn comment fix (#385)
Antonio Nikishaev
2019-09-24
Merge pull request #380 from pi8027/ring-core-scope
Cyril Cohen
2019-09-18
Fix a typo: ring_core_scope -> ring_scope
Kazuhiko Sakaguchi
2019-09-16
fermat little theorem
thery
2019-09-05
Redirects to math-comp.github.io
Cyril Cohen
2019-08-12
Merge pull request #376 from erikmd/fix-gitlab-yaml
Cyril Cohen
2019-08-10
fix(.gitlab-ci.yml): duplicated "variables:" entry
Erik Martin-Dorel
2019-08-02
Merge pull request #373 from erikmd/improve-ci
Cyril Cohen
2019-07-30
[ci] Adapt the GitLab CI config to allow scheduled builds for coq-dev
Erik Martin-Dorel
2019-07-30
[ci] Add jobs {ci-fourcolor-8.9, ci-odd-order-8.9}
Erik Martin-Dorel
2019-07-30
refactor: deploy jobs need not clone the repo
Erik Martin-Dorel
2019-07-29
style: fix indentation detail
Erik Martin-Dorel
2019-07-11
Merge pull request #369 from thery/totient
Cyril Cohen
2019-07-10
totient for prime
thery
2019-07-05
feat(finfun.v): Add tuple_of_finfun, finfun_of_tuple & cancel lemmas
Cyril Cohen
2019-06-26
Merge pull request #364 from erikmd/update/changelog
Cyril Cohen
2019-06-26
docs: Add missing entry in CHANGELOG.md
Erik Martin-Dorel
2019-06-18
Merge pull request #340 from pi8027/hierarchy
Enrico
2019-06-11
Merge pull request #302 from CohenCyril/fixset
Georges Gonthier
2019-06-04
Fixpoint theorems in finset
Cyril Cohen
2019-05-29
Merge pull request #353 from anton-trunov/update-ci
Cyril Cohen
2019-05-29
Replace eqVneq to destruct both x == y, but also y == x (#351)
Cyril Cohen
2019-05-29
Remove support for Travis CI
Anton Trunov
2019-05-29
Update pull_request_template.md
Cyril Cohen
2019-05-29
Merge pull request #352 from CohenCyril/pr_tempate
Cyril Cohen
2019-05-29
reword entry in CHANGELOG_UNRELEASED.md
Anton Trunov
2019-05-29
Update pull_request_template.md
Cyril Cohen
2019-05-29
Move unreleased changelog entries to CHANGELOG_UNRELEASED.md
Anton Trunov
2019-05-29
pr template
Cyril Cohen
2019-05-29
incorporate new suggestions by @CohenCyril
Anton Trunov
2019-05-29
Replace eqVneq with eqPsym
Anton Trunov
2019-05-29
Canonical way of expressing dis-equality on an eqType is x != y
Anton Trunov
2019-05-29
Rename eqsP to eqPsym as suggested by @CohenCyril
Anton Trunov
2019-05-28
Add eqsP view to destruct not only x == y, but also y == x
Anton Trunov
2019-05-22
htmldoc regenerated
Enrico Tassi
2019-05-22
typo
Enrico
2019-05-22
Update CHANGELOG.md
Georges Gonthier
2019-05-22
Update INSTALL.md
Enrico
2019-05-22
be explicit about opam version 2.x
Enrico
2019-05-22
Update README.md
Cyril Cohen
2019-05-21
Update CHANGELOG.md
Cyril Cohen
2019-05-17
Merge pull request #345 from math-comp/perm-tally
Georges Gonthier
2019-05-17
refactor `seq` permutation theory
Georges Gonthier
2019-05-08
Merge pull request #344 from soraros/ssrnat-remove-arith-lemmas
Georges Gonthier
2019-05-08
suppress use of `Arith` hints
Sora Chen
2019-05-06
Merge pull request #342 from math-comp/deprecation
Georges Gonthier
2019-05-06
add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma names
Georges Gonthier
2019-04-30
Ad-hoc fix
Kazuhiko Sakaguchi
2019-04-30
Reimplement the hierarchy related tools in OCaml
Kazuhiko Sakaguchi
[prev]
[next]