Pierre-Marie Pédrot
Pierre-Marie Pédrot
I don't see how you can do it without hacking the lbound at some point, though.
I definitely want to refine the criterion to rely on sort qualities in the future, but this is a quick (and dirty) cleanup that ensures that nobody can rely on...
@coqbot merge now
@coqbot bench
@silene tweak implemented. Let's @coqbot bench to see whether this affects the VM somehow.
~~I'm quite concerned that this last change in inlining will affect negatively #19014. Code generated by tactics typically contain a lot of let-bindings whose body is pretty much arbitrary (typically,...
This optimization tweak seems to impact fourcolor to some extent, but I think that the diff is small enough that we can just accept it. Otherwise I think we can...
I argue for merging as this, especially because it unlocks a tremendous reduction of the size of degenerate vo files in the dependent PR #19014.
@coqbot run full ci
@coqbot bench