diff options
| author | Guillaume Melquiond | 2021-02-12 18:11:52 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-02-23 16:02:05 +0100 |
| commit | f89f0eb4717b64f10bdd0a0edc9e93b949bcb33d (patch) | |
| tree | 305c16a4266ac19f206d4091dbb1925b2bca1a36 /kernel/vconv.ml | |
| parent | a2938972537389b9813794147412f51494f48dd1 (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 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 1432fb9310..d31d7a03b6 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -196,8 +196,9 @@ let vm_conv_gen cv_pb env univs t1 t2 = TransparentState.full env univs t1 t2 else try - let v1 = val_of_constr env t1 in - let v2 = val_of_constr env t2 in + let sigma _ = assert false in + let v1 = val_of_constr env sigma t1 in + let v2 = val_of_constr env sigma t2 in fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) with Not_found | Invalid_argument _ -> warn_bytecode_compiler_failed (); |