index
:
coq-mathcomp
master
Library of mathematical components formalized in Coq
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
CHANGELOG_UNRELEASED.md
Age
Commit message (
Expand
)
Author
2021-01-25
Merge pull request #696 from CohenCyril/sumnB
Yves Bertot
2021-01-22
Merge pull request #686 from pi8027/drop-coq-8.10
Cyril Cohen
2021-01-22
Remove deprecation aliases introduced in 1.9.0
Kazuhiko Sakaguchi
2021-01-19
Update CHANGELOG_UNRELEASED.md
Cyril Cohen
2021-01-19
Adding lemma sumnB
Cyril Cohen
2021-01-19
fixes #694
Reynald Affeldt
2021-01-16
Drop support for Coq 8.10 and deprecate the `deprecate` notation
Kazuhiko Sakaguchi
2021-01-14
itv_bound comparison with -oo/+oo
Reynald Affeldt
2021-01-12
Merge pull request #680 from pi8027/pairwise
Cyril Cohen
2020-12-16
Change the interpretation scope of some nullary notations from ring_scope to ...
Kazuhiko Sakaguchi
2020-12-16
Add `pairwise r xs` predicate
Kazuhiko Sakaguchi
2020-11-26
Regrouping changelog entries for 1.12 release
Cyril Cohen
2020-11-25
Using `only printing` and fixing coercion in notations
Cyril Cohen
2020-11-25
Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entries
Kazuhiko Sakaguchi
2020-11-25
Merge pull request #601 from pi8027/sorting_in
Cyril Cohen
2020-11-24
Transpose `join_idP(l|r)` lemmas to follow the naming convention (#671)
Kazuhiko Sakaguchi
2020-11-24
Add more `_in` lemmas and CHANGELOG entries
Kazuhiko Sakaguchi
2020-11-24
Fix `@maxr` and `@minr`
Kazuhiko Sakaguchi
2020-11-20
Tuning simplifications using Arguments simpl nomatch
Cyril Cohen
2020-11-19
Rename `subseq_order_path` to `subseq_path`
Kazuhiko Sakaguchi
2020-11-19
Refactor, reshuffle, and rename sorting lemmas in `path.v`
Kazuhiko Sakaguchi
2020-11-18
Merge pull request #651 from CohenCyril/merge_sort_push_invariant
Cyril Cohen
2020-11-18
Merge pull request #599 from CohenCyril/dup_swap_apply
Enrico Tassi
2020-11-18
Adding size_merge_sort_push
Cyril Cohen
2020-11-16
Maximal rank and full rank row submatrices
Cyril Cohen
2020-11-16
Merge pull request #636 from CohenCyril/fix_comm_mxC
Laurent Théry
2020-11-13
Merge pull request #646 from pi8027/rename-eq_sorted
Cyril Cohen
2020-11-13
Rename `eq_sorted` lemmas to `sorted_eq` and generalize `sort_le_id`
Kazuhiko Sakaguchi
2020-11-13
Fix CHANGELOG_UNRELEASED.md
Kazuhiko Sakaguchi
2020-11-12
Apply suggestions from Kazuhiko
Cyril Cohen
2020-11-12
Equivalences instead of implications for `count_maskP` and `count_subseqP`
Cyril Cohen
2020-11-12
Shorter proofs and suggestions by Kazuhiko
Cyril Cohen
2020-11-12
Adding some theory for `rem` and generalizing `subset_maskP`
Cyril Cohen
2020-11-11
Intro pattern extensions for dup, swap and apply
Cyril Cohen
2020-11-11
Apply suggestions from code review
Christian Doczkal
2020-11-11
fixup after feedback from Cyril
Christian Doczkal
2020-11-11
suggestions from Cyril
Christian Doczkal
2020-11-11
lemmas on subseq and rot
Christian Doczkal
2020-11-11
Merge pull request #632 from pi8027/path-cycle-sorted
Cyril Cohen
2020-11-11
New lemmas about allpairs
Cyril Cohen
2020-11-11
Remove `cycle_(mask|filter)` lemmas
Kazuhiko Sakaguchi
2020-11-10
Reorganize, generalize, and add lemmas about `path`, `cycle`, and `sorted`
Kazuhiko Sakaguchi
2020-11-09
fix changelog
Cyril Cohen
2020-11-09
`comm(Cmx|_mxC)` -> `comm(_scalar_mx|_mx_scalar)`
Cyril Cohen
2020-11-07
Merge pull request #626 from CohenCyril/inj_card_bij
Kazuhiko Sakaguchi
2020-11-04
Remove the `mc_1_9` compat module
Kazuhiko Sakaguchi
2020-11-04
Merge pull request #603 from chdoc/rot-rot
Kazuhiko Sakaguchi
2020-11-03
Generalizing inj_card_onto and inj_card_bij.
Cyril Cohen
2020-11-02
Adding `permS01`
Cyril Cohen
2020-11-02
lemmas for reasoing about "rot n (rot m s)"
Christian Doczkal
[next]