Guillaume Melquiond

I am not quite convinced by some of these proposals, but it might be because I don't fully understand them. I am fine with commands such as `Set Version 8.6`...

> would rather have dynamic binding be replaced by explicit option passing using optional/labeled arguments? On the OCaml side, yes, since I don't know any better way to do that....

Two preliminary remarks: - Do not add new VM opcodes (especially some that will cause an instant segfault). Use existing opcodes instead. For example, `PString.cat` can directly be mapped to...

The `CHECK` part means that they support open terms as input. (It happens that this is the most common behavior, and it would have been better to use a `NOCHECK`...

> since `char` builds in the fact that the integer value is less than 256 Note that this is not even an intrinsic property of your type. It is just...

> What are the constant factor speedups that we see for each operation? I performed a small test by repetitively concatenating strings of various size until the total size reaches...

I am a bit confused as to why there is a slowdown. The only explanation I can think of is that the code contains the following kind of construct: ```coq...

So, on the whole bench, the overall reduction of the .vo size is about 20%, with files from HoTT being reduced by more than 70% (?!).

Sure. But think about it. By design, this patch cannot perform a better compression than 75% of the bytecode segment of a .vo file (and in practice, it is more...

As an illustration, here is what the factorial function of the standard library looks like before and after this patch. Before, 240 bytes: ``` 2c 00 00 00 01 00...