Skip to content

Pull requests: math-comp/math-comp

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
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort

Pull requests list

fix already merged PR #1587
#1588 opened Apr 25, 2026 by affeldt-aist Member Loading…
4 tasks
Documented but missing notations
#1586 opened Apr 24, 2026 by affeldt-aist Member Loading…
1 of 4 tasks
2.6.0
Adapt to https://github.com/rocq-prover/rocq/pull/21947
#1585 opened Apr 23, 2026 by proux01 Contributor Draft
Rename all_foo.v -> foo.v needs: merge of dependencies PR that depends on another. Documented in the original post of the PR. Review only the increment.
#1582 opened Apr 21, 2026 by proux01 Contributor Loading…
2 of 4 tasks
2.6.0
Rename packages fingroup -> group and character -> group-representation
#1581 opened Apr 21, 2026 by proux01 Contributor Loading…
2 of 4 tasks
2.6.0
[WIP] 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 Draft
8 tasks
2.7.0
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
Tensor formalization
#1535 opened Feb 12, 2026 by hoheinzollern Member Loading…
2 of 4 tasks
2.6.0
HB.pack -> HB.enrich
#1511 opened Dec 21, 2025 by gares Member Draft
More Archimedean lemmas
#1510 opened Dec 4, 2025 by pi8027 Member Draft
4 tasks
2.7.0
lra/nra/psatz/ring/field without Stdlib
#1456 opened Aug 27, 2025 by proux01 Contributor Loading…
21 tasks done
2.6.0
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
[Draft] Add extended real numbers
#1338 opened Feb 5, 2025 by CohenCyril Member Draft
7 tasks
2.6.0
Characteristic for all
#1308 opened Nov 29, 2024 by Tragicus Contributor Draft
4 tasks done
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.6.0
Remove the phantom in tuple
#1200 opened Mar 29, 2024 by CohenCyril Member Draft
4 tasks
2.6.0
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+
Inductive principles on set cardinality
#1120 opened Nov 6, 2023 by pPomCo Contributor Loading…
3 of 4 tasks
2.6.0
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.6.0
Contrib finset
#1118 opened Nov 6, 2023 by pPomCo Contributor Loading…
2 of 4 tasks
2.6.0
ProTip! Type g i on any issue or pull request to go back to the issue listing page.