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
2020-08-26
Update pull_request_template.md
Cyril Cohen
2020-08-20
Merge pull request #550 from jashug/dont-refresh-argument-names-overlay
Enrico Tassi
2020-08-17
Merge pull request #547 from pi8027/qualified-dual-op
Cyril Cohen
2020-08-17
Qualify the dual_* notations with the Order module
Kazuhiko Sakaguchi
2020-08-16
Merge pull request #517 from thery/minn
Cyril Cohen
2020-08-15
Extra theorems about subn min and max
thery
2020-08-13
Be robust to a change in the default argument naming algorithm.
Jasper Hugunin
2020-08-13
Merge pull request #545 from pi8027/fieldext
Cyril Cohen
2020-08-13
Merge pull request #553 from chdoc/non-reversible-notation
Cyril Cohen
2020-08-13
Merge pull request #494 from pi8027/rm-displays-in-classes
Cyril Cohen
2020-08-13
fix non-reversible-notation warnings
Christian Doczkal
2020-08-12
Make [fieldExtType F of L] work for abstract instances
Kazuhiko Sakaguchi
2020-08-12
Get rid of displays in class fields and mixin parameters
Kazuhiko Sakaguchi
2020-08-11
Merge pull request #552 from chdoc/rel-format-warning
Cyril Cohen
2020-08-11
fix notation-incompatible-format warnings
Christian Doczkal
2020-08-11
Merge pull request #507 from pi8027/test-guard-cond
Cyril Cohen
2020-08-11
Merge pull request #542 from chdoc/nothing-to-inject
Cyril Cohen
2020-08-11
Merge pull request #551 from CohenCyril/merge-changelog-by-union
Cyril Cohen
2020-08-11
Use union driver for CHANGELOG_UNRELEASED
Cyril Cohen
2020-08-11
Merge pull request #541 from chdoc/properC
Cyril Cohen
2020-08-11
Merge pull request #536 from pi8027/hierarchy
Cyril Cohen
2020-06-27
Fix some Makefile issues and rename `hierarchy_test.v` to `test_hierarchy_all.v`
Kazuhiko Sakaguchi
2020-06-27
Fix bugs in hierarchy.ml
Kazuhiko Sakaguchi
2020-06-26
fix "Nothing to inject" warnings
Christian Doczkal
2020-06-26
lemmas for proper and setC
Christian Doczkal
2020-06-24
Merge pull request #540 from thery/doc
Cyril Cohen
2020-06-24
Merge pull request #539 from thery/sum_nat_const
Cyril Cohen
2020-06-24
missing bigop lemmas (#537)
Laurent Théry
2020-06-24
missing lemmas discovered while developing mathcomp-analysis
Reynald Affeldt
2020-06-24
fix the doc for ubnP in ssrnat
thery
2020-06-24
simpler proof
thery
2020-06-19
Merge pull request #509 from chdoc/card-lemmas
Cyril Cohen
2020-06-18
conform to 80 chars limit
Christian Doczkal
2020-06-18
fixup spacing
Cyril Cohen
2020-06-18
Apply suggestions from code review
Christian Doczkal
2020-06-18
drop_uniq / CHANGELOG
Christian Doczkal
2020-06-18
add fcard_gt?P lemmas found in fourcolor
Christian Doczkal
2020-06-18
cards_eqP and cards2P
Christian Doczkal
2020-06-18
cardinality lemmas for #|A| <= 1 and n <= #|A|
Christian Doczkal
2020-06-17
Merge pull request #499 from chdoc/contra-prop
Cyril Cohen
2020-06-17
contra lemmas involving propositions
Christian Doczkal
2020-06-13
Add more test cases for higher-order recursive functions in seq.v w.r.t. the ...
Kazuhiko Sakaguchi
2020-06-10
Merge pull request #535 from CohenCyril/allow-coq-dev
Cyril Cohen
2020-06-10
Generated opam packages allow coq-dev again
Cyril Cohen
2020-06-09
removing opam `| (= "dev")` for released packages
Cyril Cohen
2020-06-09
Complying to SPDX
Cyril Cohen
2020-06-09
fixing mailmap
Cyril Cohen
2020-06-09
mailmap for Yves and Reynald
Cyril Cohen
2020-06-09
Merge pull request #533 from affeldt-aist/changelogs_before_release
affeldt-aist
2020-06-09
Merge pull request #534 from CohenCyril/doc-1.11
Cyril Cohen
[next]