Guillaume Melquiond

I am not really concerned about performance. I am more interested in knowing whether we still need a followup pull request that uses a bitvector instead of an array of...

It matters because some `.vo` files have grown by several tens of kilobytes. So, I dispute your "typically small".

Does that ring a bell? ``` [ERROR] The compilation of coq-test-suite.dev failed at "dune build -p coq -j 1 --promote-install-files=false @runtest". ... - output/ltac2_unused_var.v...Error! (unexpected output) ... - File "./bugs/bug_11766.v",...

@coqbot run full ci

@coqbot bench

The bench unfortunately failed to complete due to concurrent commits in the tested repositories, but it still gives an idea. As with #18964, the overall gain is minor, but specific...

After the merge of #18968, the benefits of this pull request increase notably, at least for `coq-hott`. For example, the size reduction of `Products.vo` now reaches 32% (instead of 18%),...

@coqbot run full ci

@coqbot bench

> Shouldn't the error be on the false, rather than the 0? Coq stops as soon as it detects a typing error, so it does not even reach the point...