Conversation
pi8027
changed the title
pi8027
force-pushed
the
semi-poly
branch
2 times, most recently
from
4000dbd to
2c60cf5
Compare
pi8027
force-pushed
the
semi-poly
branch
2 times, most recently
from
31592c9 to
61d1397
Compare
|
CI green |
|
I just updated the comment in the hope we'll find it by greping 2.4.0 in the future (that's usually what I do when dropping Coq support in mathcomp, although I must admit it's less likely I'll ever do it here) |
|
I have the impression that odd-order can benefit from the stuff recently added to MathComp, e.g., the first commit of this PR. It would be great if we could take a look at the proofs and clean them up every few years. (Indeed, the problem is that no one has time to do this kind of low-priority and time-consuming task.) |
|
Considering odd-order is rather a leaf in the dependency tree (I'm not sure anyone really depend on it), I guess it would be fine to have it only compile with the last mathcomp. So as soon as 2.4.0 is out, feel free to drop support for any older mathcomp and take advantage of the recent stuffs to do any simplification here. |
2 participants
Adapt to math-comp/math-comp#1395