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-04-06
Merge pull request #472 from affeldt-aist/doc_fix
Yves Bertot
2020-04-06
minor documentation fix
Reynald Affeldt
2020-04-02
Merge pull request #468 from ybertot/remove-deprecated-from-1.9
Enrico Tassi
2020-04-01
Merge pull request #429 from pi8027/extend-nat-comparison
Yves Bertot
2020-03-31
remove deprecated commands whose deprecation was introduced in release 1.9.0
Yves Bertot
2020-03-31
Merge pull request #457 from CohenCyril/find
Yves Bertot
2020-03-19
Merge pull request #463 from pi8027/hierarchy-transitive-closure
Enrico Tassi
2020-03-18
Merge pull request #459 from CohenCyril/sub_sorted
Cyril Cohen
2020-03-16
Update mathcomp/ssreflect/path.v
Cyril Cohen
2020-03-16
Link between subrelations and path/sorted
Cyril Cohen
2020-03-16
Document change on comparison predicates in order.v
Kazuhiko Sakaguchi
2020-03-16
Merge pull request #460 from affeldt-aist/spurious_lerr
Cyril Cohen
2020-03-15
just noticed a tentative use of a not yet existing lemma
Reynald Affeldt
2020-03-15
Reorder arguments of comparison predicates in order.v as they should
Kazuhiko Sakaguchi
2020-03-15
Extend comparison predicates for nat with minn and maxn
Kazuhiko Sakaguchi
2020-03-15
Fix hierarchy.ml to compute the transitive closure of a hierarchy
Kazuhiko Sakaguchi
2020-03-12
Merge pull request #465 from erikmd/coq-8.11
Cyril Cohen
2020-03-12
Merge pull request #455 from erikmd/bump-opam
Cyril Cohen
2020-03-08
[ci] Build mathcomp/mathcomp-dev:8.11
Erik Martin-Dorel
2020-03-08
Fix CI (coq-lemma-overloading dropped compatibility with Coq < 8.10)
Erik Martin-Dorel
2020-03-08
refactor: Simplify the Dockerfiles
Erik Martin-Dorel
2020-01-30
Merge pull request #453 from pi8027/experiment/order-nondistr-lattice
Pierre-Yves Strub
2020-01-29
Documentation work for (non-distributive) latticeType
Kazuhiko Sakaguchi
2020-01-28
Added lemmas about foldl, scanl, foldr and rcons and cons
Cyril Cohen
2020-01-28
Theorems about find and index
Cyril Cohen
2020-01-21
Merge pull request #452 from SimonBoulier/non_maximal_implicit
Enrico Tassi
2020-01-17
Revert "Don't run "opam clean -c" to workaround ocaml/opam#3828"
Erik Martin-Dorel
2020-01-15
Non-distributive lattice
Kazuhiko Sakaguchi
2020-01-14
Merge pull request #454 from CohenCyril/dual
Cyril Cohen
2020-01-10
Missing canonical structures for dual
Cyril Cohen
2020-01-10
Exporting T^d notation
Cyril Cohen
2020-01-09
Renaming converse to dual in order.v
Cyril Cohen
2020-01-09
Merge pull request #435 from anton-trunov/add-fcsl-pcm-to-ci
Enrico Tassi
2020-01-08
Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)
SimonBoulier
2020-01-07
Add FCSL-PCM library to CI
Anton Trunov
2020-01-03
Merge pull request #443 from pi8027/eqVneq
Cyril Cohen
2019-12-28
Refactoring and linting especially polydiv
Kazuhiko Sakaguchi
2019-12-26
Merge pull request #450 from pi8027/remove-ci-overlay-270
Cyril Cohen
2019-12-18
Remove CI overlay for PR #270
Kazuhiko Sakaguchi
2019-12-17
Merge pull request #451 from erikmd/fix-scheduled-ci
Cyril Cohen
2019-12-15
fix: Add missing "except: schedules"
Erik Martin-Dorel
2019-12-11
Merge pull request #445 from ybertot/opam-packages
Enrico Tassi
2019-12-11
Merge pull request #270 from math-comp/experiment/order
Assia Mahboubi
2019-12-11
The compatibility module in ssrnum should now be for version 1.10
Kazuhiko Sakaguchi
2019-12-11
Rephrasing the doc
Cyril Cohen
2019-12-11
remove ProdNormedZmodule (#419)
affeldt-aist
2019-12-11
renaming NormedZmoduleType and NormedZmoduleMixin (#416)
affeldt-aist
2019-12-11
Fix notation modifiers and scopes
Kazuhiko Sakaguchi
2019-12-11
Doc, comments, changelog and better proofs
Cyril Cohen
2019-12-11
Comparability in a numDomainType
Cyril Cohen
[next]