Quentin VERMANDE
Quentin VERMANDE
There was a broken url, which I expect made the bench fail. It should be fixed now.
May I ask for a bench?
I added `coq-mathcomp-classical` (and not `coq-mathcomp-analysis` as the error message suggests) to the opam configuration files for the bench in `opam-coq-archive`. I do not understand what is wrong with the...
All right, is there a way to finish the bench without losing the progress?
I mean that losing 10 hours of compilation is a bit sad, so I hope there is a way to restart the bench at `coq-mathcomp-classical` where it stopped.
Not off the top of my head, but there is a trivial solution, which is giving an empty list of structures to the directive.
> What is the justification for the mandatory addition of constants for the application of `blah_cst` lemmas? Do we know where the problem comes from? `cst` is not dependent (and...
I extracted this from the other PR and extended it when I realized I needed to generalize things here first. It is ready for review.
Yes, sure, in the end it will be generalized to `pzSemiRingType` but we can get `nzSemiRingType` now basically for free.
https://github.com/rocq-prover/rocq/pull/20730 is 0.3% slower on `master` and 5% faster on this branch (than `rocq/master`). With the Rocq PR, this branch becomes 1% slower than `master`.