Matthieu Sozeau

@coqbot bench

@ppedrot @SkySkimmer on current master this has a negligible effect, however on top of algebraic universes, math-classes goes from 149s to 123s just by forcing `equiv` and `le/lt` to unfold...

Yep

Indeed, refine pierces through Opacified Defined constants (so we keep SR)... For evarconv Opaque just means unfold at last resort.

@coqbot run full ci

I backtracked on changing the default, too much incompatibilities arise. If one changes it from "-" to "!" or "+" it will generally incur more failed typeclass searches (or speedups...

Agreed @TheoWinterhalter, that was the original motivation of this PR to be able to set the default mode to "!" in GoodDefaults :)

@coqbot run full ci

I backtracked on trying to change the default or any mode declaration in the stdlib to ensure compatibility for now.

@coqbot run full ci