The Wayback Machine - https://web.archive.org/web/20201211000617/https://github.com/math-comp/math-comp/pulls
Skip to content

/ math-comp

New pull request New
21 Open 434 Closed
21 Open 434 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels.
Projects
Filter by project
Milestones
Filter by milestone
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀
Remove ci-fcsl-pcm-8.10
kind: CI
#683 opened Dec 5, 2020 by pi8027
Rework of PR #281: Archimedean structures on top of num/real domain/field/closedField
kind: enhancement needs: fix
#682 opened Dec 3, 2020 by pi8027 • Draft 0 of 2
9
Add `pairwise` predicate and some missing lemmas
kind: enhancement
#680 opened Dec 2, 2020 by pi8027 2 of 2
2
1
Using Arguments simpl never instead of nosimpl
kind: refactoring
#660 opened Nov 20, 2020 by CohenCyril • Approved 1.15.0
1
@affeldt-aist
12
[WIP] Make linear subspaces canonically a `tbLatticeType`
kind: enhancement kind: refactoring needs: fix
#653 opened Nov 19, 2020 by pi8027 • Draft 0 of 2 1.13.0
1
4
Renaming matrix lemmas
#652 opened Nov 18, 2020 by CohenCyril 1 of 1 1.13.0
1
1
Add sorting lemmas specialized for `porderType` and `orderType`
kind: enhancement
#649 opened Nov 13, 2020 by pi8027 • Draft 1 of 1 1.13.0
1
2
Use predicators even extensively
needs: fix
#548 opened Jul 16, 2020 by pi8027 • Draft 0 of 1
3
Adding only parsing to notations in ssrAC
#527 opened Jun 8, 2020 by CohenCyril • Draft
closed/closure for non-symmetric relations
#503 opened May 11, 2020 by chdoc 0 of 3 1.13.0
1
@CohenCyril
2
Intro discharge subst
drops: coq 8.9
#502 opened May 8, 2020 by CohenCyril • Draft 2 of 4
Intro pattern extensions for rewrite, dup, swap and apply
drops: coq 8.9 kind: enhancement
#501 opened May 8, 2020 by CohenCyril • Draft 2 of 3 1.13.0
@gares
8
New order structures and definitionally involutive duals
kind: enhancement
#464 opened Mar 4, 2020 by pi8027 3 of 3
18
[teaching] Mini MC
#461 opened Feb 21, 2020 by gares
Multisets library
kind: enhancement needs: assignee needs: merge of dependencies
#354 opened May 29, 2019 by CohenCyril • Draft 2 of 2 1.13.0
2
Make the finType structure equipped with indexing functions
needs: assignee needs: rebase
#317 opened Apr 1, 2019 by pi8027 • Draft
2
[build] Support for building with Dune.
#316 opened Mar 30, 2019 by ejgallego • Changes requested 1.13.0
@gares
25
[WIP] Archimedean structures on top of num/real domain/field/closedField
#281 opened Feb 7, 2019 by Sobernard • Draft 1.13.0
@pi8027
9
Adding finmap to mathcomp
kind: enhancement kind: refactoring
#259 opened Dec 10, 2018 by CohenCyril • Draft 3 of 3 1.13.0
@gares
27
The vector space of bounded degree polynomials
kind: enhancement needs: fix
#210 opened Jul 28, 2018 by CohenCyril • Draft 2 of 3 1.13.0
18
Work In Progress: adding forms and spectral theorems
kind: enhancement needs: more development
#207 opened Jul 27, 2018 by CohenCyril • Draft 2 of 9 1.13.0
ProTip! Follow long discussions with comments:>50.
You can’t perform that action at this time.