Quentin VERMANDE
Quentin VERMANDE
May I ask for a bench?
Actually, if there is a way to reduce `GRing_Nmodule__to__GRing_AddMagma ssrint_int__canonical__GRing_Nmodule` to `ssrint_int__canonical__GRing_AddMagma` without mentioning `addMagmaType` and with a code that works on the current version of MC (i.e. when there...
As your tests show, the sort coercion postcomposes and does not precompose with Coq's coercions. This is because when the algorithm sees that the type of the input term is...
A use case for something that is not a structure coercing to a structure is when you have an object that satisfies properties that would promote it to a structure,...
Do we have tools to do a benchmark?
Ok thanks, I will do that tonight or tomorrow.
It took forever, but the bench is done. Interestingly enough, the version with typeclasses by default is slightly slower and uses slightly less memory, though the difference is negligible. [bench.ods](https://github.com/user-attachments/files/16041714/bench.ods)...
Well, I did it anyway, and `master` is about 3x faster than `proto-coercion`. [bench.ods](https://github.com/user-attachments/files/16043833/bench.ods).
Here is the new bench, `proto-coercion` is a little less than 2x slower than `master`. The profiling might be complicated since the slowdown occurs in tactics like `apply:`. [benchcoe.ods](https://github.com/user-attachments/files/16415657/benchcoe.ods)
Ah, if that comes from a configuration issue on my side, it might be easy to solve, although I do not know what to look for. I indeed got the...