Skip to content

Issues: math-comp/math-comp

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

99 Open 221 Closed
99 Open 221 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Search in directive does not interact well with submodules designed for opacification
#1220 opened May 29, 2024 by CohenCyril
Nix CI of MathComp should run the test suites of Mczify and Algebra Tactics
#1219 opened May 28, 2024 by pi8027
7
FalgType or falgType
#1208 opened Apr 10, 2024 by pi8027
Provide column vector versions of defs/lemmas in mxalgebra and vector
#1204 opened Apr 5, 2024 by proux01
Sharing bigop lemmas between monoids and idempotent semigroups (bands) kind: enhancement Issue or PR about addition of features.
#1189 opened Mar 25, 2024 by pi8027
5
Add subobjects in the category of posets
#1187 opened Mar 22, 2024 by proux01
Avoid exporting warning settings
#1158 opened Jan 17, 2024 by proux01 2.3.0
Check MC1 backports
#1154 opened Jan 15, 2024 by proux01 1.20.0
2
Bind Scope declarations for structure record types
#1136 opened Dec 8, 2023 by pi8027
Detailed installation instructions with make
#1129 opened Nov 28, 2023 by chirag03k
2
Refactor qpoly and poly kind: refactoring Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...)
#1128 opened Nov 27, 2023 by pi8027
2
Incoherence of the implicit status of lemmas
#1127 opened Nov 17, 2023 by pi8027
6
Semi-modules and semi-algebras kind: enhancement Issue or PR about addition of features.
#1124 opened Nov 14, 2023 by pi8027
1
@pi8027
3
Disable warning about redundant projection
#1113 opened Nov 2, 2023 by thery
rpred expose the iinternal of Num.real
#1108 opened Oct 25, 2023 by thery
5
does leq_subr follow the naming convention?
#1093 opened Oct 11, 2023 by affeldt-aist
Performance problem with multiple rewrite in mathcomp2
#1091 opened Oct 5, 2023 by thery
1
Naive parametric instance problem
#1090 opened Oct 5, 2023 by thery
5
vm_compute getting very slow
#1088 opened Oct 4, 2023 by thery
14
Investigate slowness of mathcomp's vs. coq's GitLab CI builds kind: CI Issue or PR about the CI. (Gitlab CI or CI of dependencies problems linked with math-comp)
#1078 opened Sep 20, 2023 by erikmd
Investigate HB-related slowdown in has_prim_root_subproof
#1067 opened Sep 6, 2023 by CohenCyril
Replace some factories by functions
#1024 opened May 17, 2023 by CohenCyril
1
De-deprecate and rename
#1015 opened May 9, 2023 by CohenCyril
Create documentation for eqVneq as a preferred way to perform case analysis on boolean equality
#1005 opened May 3, 2023 by ybertot
rpredM for subalgebras
#996 opened Apr 14, 2023 by Tragicus
1
ProTip! no:milestone will show everything without a milestone.