Guillaume Melquiond
Guillaume Melquiond
Duplicate of #14405.
> the error message should not say "Please report", it should say, "Coq cannot work without an environment variable `OCAMLFIND_CONF` set You might be missing an important point. As explained...
@SkySkimmer No, it is the same. (That said, the location of the casts in the produced proof term might be slightly different. I never remember the precise rules for `change`,...
> we do not have to load in memory potentially huge relocations at require time, One thing I don't understand is that the bench shows absolutely zero change in the...
As this is still a draft, I am postponing it to 8.15.
Since it only fixes one of the three issues listed in #18703 (only `Cast`, neither `Array` nor `Prod`), please remove the "Fixes" line from your original message, so that Github...
Yes, but for your example, it is debatable whether `large` should be or not be evaluated, since it occurs in the term. Indeed, there is nothing wrong with a call-by-value...
In addition to casts and primitive arrays, left-hand sides of products are also characterized incorrectly and can cause spurious blowups. (That is, a product should be characterized as computational if...
And it appears that plain constants are also sufficient to crash Coq: ```coq Fixpoint fact n := match n with S n' => n * fact n' | O =>...