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
2018-12-13
Adjust implicits of cancellation lemmas
Georges Gonthier
2018-12-12
Gitter Badge
Cyril Cohen
2018-12-11
Merge pull request #260 from CohenCyril/fix_TFAE
Laurence
2018-12-11
Merge pull request #252 from anton-trunov/implicit-core-hint-db
Cyril Cohen
2018-12-11
Fix some new warnings emitted by Coq 8.10:
Anton Trunov
2018-12-11
Merge pull request #257 from CohenCyril/eqmsP
Georges Gonthier
2018-12-11
fix TFAE
Cyril Cohen
2018-12-10
Adding lemma `eqmxMunitP`
Cyril Cohen
2018-12-10
Merge pull request #248 from anton-trunov/remove-Type-from-packed-classes
Cyril Cohen
2018-12-06
Update ChangeLog
Anton Trunov
2018-12-04
Remove pack constructors
Anton Trunov
2018-12-04
Remove `_ : Type` from packed classes
Anton Trunov
2018-12-04
Merge pull request #253 from anton-trunov/arguments
Georges Gonthier
2018-12-04
Document parameter names whenever possible
Anton Trunov
2018-11-26
correct and improve signature and documentation of FieldMixin
Georges Gonthier
2018-11-24
Merge pull request #249 from anton-trunov/prenex-implicits
Cyril Cohen
2018-11-21
Merge Arguments and Prenex Implicits
Anton Trunov
2018-11-19
Improve documentation of phant_id usage
Georges Gonthier
2018-11-19
Merge pull request #242 from anton-trunov/remove-canonical-for-mixins
Georges Gonthier
2018-11-15
Merge pull request #246 from anton-trunov/doc-comments
Cyril Cohen
2018-11-15
Tweak code related to canonical mixins
Anton Trunov
2018-11-15
Add a section on documenting code
Anton Trunov
2018-11-13
Documentation complements for combinatorial class factories
Georges Gonthier
2018-11-13
Ignore generated Makefile.coq.conf
Georges Gonthier
2018-11-06
Merge pull request #241 from ybertot/fix240
Cyril Cohen
2018-11-05
fix issue #240
Yves Bertot
2018-10-31
Merge pull request #239 from CohenCyril/Make_bug
Enrico
2018-10-31
fixing local Makefile
Cyril Cohen
2018-10-30
Merge pull request #236 from CohenCyril/allsigs
Cyril Cohen
2018-10-29
Revert "Adding allsigs, the dependent version of allpairs"
Cyril Cohen
2018-10-29
Merge pull request #219 from CohenCyril/Makefile
Enrico
2018-10-26
Merge pull request #235 from CohenCyril/bool_irrelevance2
Cyril Cohen
2018-10-26
fix some bugs in Makefile
Cyril Cohen
2018-10-26
Statement of `bool_irrelevance` more consistent with its name.
Cyril Cohen
2018-10-26
Merge pull request #209 from CohenCyril/closed_field
Cyril Cohen
2018-10-26
moving countalg and closed_field around
Cyril Cohen
2018-10-26
Merge pull request #218 from CohenCyril/tagged
Cyril Cohen
2018-10-26
removing multiple definitions of [tT]ag*
Cyril Cohen
2018-10-25
Merge pull request #234 from CohenCyril/ocaml4.05.0
Enrico
2018-10-25
bump ocaml version in travis
Cyril Cohen
2018-10-25
Merge pull request #232 from anton-trunov/master
Enrico
2018-10-25
Merge pull request #217 from CohenCyril/allsigs
Laurent Théry
2018-10-24
Adding allsigs, the dependent version of allpairs
Cyril Cohen
2018-10-03
[opam]: add dev-repo links
Anton Trunov
2018-09-24
Implementation of all2 (#224)
Pierre-Yves Strub
2018-09-13
Merge pull request #216 from CohenCyril/all_iff
Assia Mahboubi
2018-09-13
Small scale tool for proving "the following are equivalent"
Cyril Cohen
2018-09-12
Merge pull request #228 from hivert/docfix
Cyril Cohen
2018-09-11
Fixes the doc of rat
Florent Hivert
2018-09-06
Merge pull request #223 from math-comp/fix/compat-notation
Assia Mahboubi
[next]