aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses_errors.ml
diff options
context:
space:
mode:
authorGuillaume Melquiond2021-02-12 18:11:52 +0100
committerGuillaume Melquiond2021-02-23 16:02:05 +0100
commitf89f0eb4717b64f10bdd0a0edc9e93b949bcb33d (patch)
tree305c16a4266ac19f206d4091dbb1925b2bca1a36 /pretyping/typeclasses_errors.ml
parenta2938972537389b9813794147412f51494f48dd1 (diff)
Normalize evars during bytecode compilation (fix #13841).
Otherwise, the interpreter sees already unified evars as accumulators rather than actual constants, thus preventing the computations from progressing. This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed evar normalization. The effect went unnoticed because the computed term is still convertible to the reduced term, except that it is the lazy machinery that ends up reducing it, rather than the bytecode one. So, performances became abysmal, seemingly at random.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions