Skip to content

Pull requests: math-comp/math-comp

New pull request New
48 Open 1,165 Closed
48 Open 1,165 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

Rename the Archimedean mixin and some lemmas (follow-up of #1510) kind: clean-up This issure/PR is about cleaning up obsolete code, removing hacks, etc
#1629 opened Jul 20, 2026 by pi8027 Member Loading…
4 tasks
2.8.0
Compatibility patch for Rocq PR #22272
#1628 opened Jul 19, 2026 by olympichek Loading…
Generalized compose of linear maps w.r.t. to change of scalar kind: enhancement Issue or PR about addition of features.
#1627 opened Jul 16, 2026 by hivert Member Loading…
1 of 4 tasks
5
[CI] Add fpseries
#1623 opened Jul 6, 2026 by proux01 Contributor Loading…
Drop support for Rocq 9.0 needs: merge of dependencies PR that depends on another. Documented in the original post of the PR. Review only the increment.
#1622 opened Jun 29, 2026 by proux01 Contributor • Draft
1
[CI] Add Coq-Combi
#1616 opened Jun 25, 2026 by proux01 Contributor Loading…
Adapt to HB/mixin-tc
#1615 opened Jun 17, 2026 by Tragicus Contributor Loading…
4 tasks
reintroducing covariant and tensor product notations
#1613 opened Jun 10, 2026 by hoheinzollern Member • Draft
4 tasks
spectral: spectral theorem for real symmetric matrices
#1611 opened Jun 5, 2026 by gbdrt Loading…
4 tasks done
1
[WIP] Add morphism instances on horner ^~ x
#1607 opened Jun 3, 2026 by pi8027 Member • Draft
4 tasks
4
[WIP] Distinguishing scalars from norm codomain
#1605 opened Jun 2, 2026 by CohenCyril Member • Draft
4 tasks
1
Use binary parser for rat Number Notation
#1602 opened May 28, 2026 by hoheinzollern Member • Draft
4 tasks
1
Remove pz (potentially-zero) kind: clean-up This issure/PR is about cleaning up obsolete code, removing hacks, etc
#1600 opened May 27, 2026 by pi8027 Member Loading…
4 tasks done
2.7.0
1
1
Adapt to rocq-prover/rocq#21987 (secvar status)
#1599 opened May 21, 2026 by SkySkimmer Contributor Loading…
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…
10 of 14 tasks
2.7.0
1
39
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
HB.pack -> HB.enrich
#1511 opened Dec 21, 2025 by gares Member • Draft
1
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
ProTip! Mix and match filters to narrow down what you’re looking for.