Pierre-Marie Pédrot
Pierre-Marie Pédrot
@coqbot merge now
Obviously, you have to import the corresponding modules for the instances to be available. Marking them global lets you do that silently through Require, but you lose any control over...
Indeed, we need a serious set of rules for adding instances to the stdlib, so that users know when and what to import. I'm afraid that these guidelines do not...
> it means that more than 98% of the file is currently occupied by the bytecode segment This is in line with some profiling I had done before, so I'm...
> the size of the bytecode is directly proportional to the size of the term This is not quite true, the current compilation scheme of closures is quadratic in the...
> it is important that a closure does not spuriously keep terms alive While I agree with this claim in your run-of-the-mill call-by-value boolean evaluator, it's not clear to me...
Good catch, I didn't think about the universe instances...
@silene can you rebase and rebench?
I took the liberty to rebase myself. @coqbot run full ci
@coqbot bench