Guillaume Melquiond

As Coq rightfully complains, the result `0` of the first branch does not have type `match ?v@{v1:=index} with index | _ => nat end`. If you write an explicit `return`...

Both your examples behave in the exact same way. The value of the first branch does not match its inferred type, so Coq complains about a type error. It never...

@coqbot bench

The overall `.vo` size reduction is rather low, of the order of 0.5% on the whole CI. That said, some developments still benefit heavily from this pull request, e.g., `coq-fiat-crypto-with-bedrock`...

Hard to tell. If the optimization triggers, the generated bytecode is a bit smaller, so it might delay the next garbage collection. But on the other hand, the allocation of...

Actually, this is a semi-pointless optimization, since a look at the assembly code shows that I had not taken into account the allocation for the pair. So, despite the latest...

@coqbot bench