Matthieu Sozeau
Matthieu Sozeau
@coqbot bench
Wow, that's huge! Require speedups are surprising to me, if anything the discrimination trees should be larger now....
@coqbot bench Now with an updated overlay
``` │ rocq-stdlib │ 430.28 448.96 -4.16 │ 1519362115463 1593360094009 -4.64 │ 617212 614848 0.38 │ ``` Ok, that seems like a more reasonable improvement :)
The stdlib test-suite shows that opacity prevents matching with eta-expansions...
@palmskog @silene this is ready now
@coqbot bench
@coqbot bench
@coqbot bench
@coqbot bench