Skip to content

Pull requests: math-comp/math-comp

New pull request New
38 Open 1,150 Closed
38 Open 1,150 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Revert "Remove [POrder of T by <:] and [Order of T by <:]"
#1598 opened May 15, 2026 by pi8027 Member Loading…
4 tasks
2.6.0
Add endless and dense orders
#1597 opened May 13, 2026 by t6s Member • Draft
4 tasks
2
Refactor the lattice instances on intervals and their bounds kind: refactoring Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...)
#1589 opened Apr 29, 2026 by pi8027 Member • Draft
4 tasks
1
Split order.v kind: refactoring Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...)
#1580 opened Apr 20, 2026 by pi8027 Member Loading…
9 of 14 tasks
2.7.0
1
22
Eliminate the dependency from orderedzmod to rings_modules_and_algebras
#1560 opened Mar 18, 2026 by pi8027 Member • Draft
4 tasks
2.7.0
1
exp -> pow (wip) kind: refactoring Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...)
#1544 opened Feb 24, 2026 by affeldt-aist Member • Draft
4 tasks
2.7.0
19
Tensor formalization needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it.
#1535 opened Feb 12, 2026 by hoheinzollern Member Loading…
3 of 4 tasks
2.6.0
46
HB.pack -> HB.enrich
#1511 opened Dec 21, 2025 by gares Member • Draft
1
More Archimedean lemmas
#1510 opened Dec 4, 2025 by pi8027 Member • Draft
4 tasks
2.7.0
1
32
lra/nra/psatz/ring/field without Stdlib
#1456 opened Aug 27, 2025 by proux01 Contributor Loading…
23 tasks done
2.6.0
15
Implemented wrapping of mixin in bigop.v for files monoid.v and nmodule.v
#1435 opened May 19, 2025 by CalosciMatteo • Draft
4 tasks
Remove the workarounds introduced in #1125 drops: coq 8.20 kind: clean-up This issure/PR is about cleaning up obsolete code, removing hacks, etc
#1365 opened Mar 19, 2025 by pi8027 Member • Draft
4 tasks
2.7.0
40
[Draft] Add extended real numbers
#1338 opened Feb 5, 2025 by CohenCyril Member • Draft
7 tasks
2.7.0
14
Characteristic for all
#1308 opened Nov 29, 2024 by Tragicus Contributor • Draft
4 tasks done
Complements to math-comp originating from the trajectories proofs
#1299 opened Nov 27, 2024 by ybertot Member • Draft
1 of 4 tasks
2.7.0
1
Fix the notation scope of function notations in ssralg (#978)
#1213 opened Apr 23, 2024 by pi8027 Member • Draft
2 of 4 tasks
1
8
falgebra and fieldext parts of CohenCyril's abel backports needs: merge of dependencies PR that depends on another. Documented in the original post of the PR. Review only the increment.
#1202 opened Apr 2, 2024 by Tragicus Contributor Loading…
3 of 4 tasks
2.7.0
3
Remove the phantom in tuple
#1200 opened Mar 29, 2024 by CohenCyril Member • Draft
4 tasks
2.7.0
7
finmap needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it.
#1138 opened Dec 11, 2023 by gares Member • Draft 100+
4
Inductive principles on set cardinality
#1120 opened Nov 6, 2023 by pPomCo Contributor Loading…
3 of 4 tasks
2.7.0
5
Contrib bigop needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it.
#1119 opened Nov 6, 2023 by pPomCo Contributor Loading…
2 of 4 tasks
2.7.0
@Tragicus
19
Contrib finset
#1118 opened Nov 6, 2023 by pPomCo Contributor Loading…
2 of 4 tasks
2.7.0
@CohenCyril
5
Fix the scope of arguments of intmul needs: fix PR that needs to be fix (generally because reviewers asked to).
#1086 opened Sep 28, 2023 by proux01 Contributor • Draft
3 of 4 tasks
2.7.0
9
Ring coercions drops: coq 8.16 drops: coq 8.17
#1051 opened Jul 18, 2023 by proux01 Contributor • Draft
1 of 4 tasks
17
Abel backports
#944 opened Nov 29, 2022 by CohenCyril Member • Draft
2 tasks
31
ProTip! no:milestone will show everything without a milestone.