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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/vnorm.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index cf6d581066..5622bd357a 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -414,9 +414,9 @@ let cbv_vm env sigma c t = if Termops.occur_meta sigma c then CErrors.user_err Pp.(str "vm_compute does not support metas."); (* This evar-normalizes terms beforehand *) - let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in - let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in - let v = Vmsymtable.val_of_constr env c in + let c = EConstr.Unsafe.to_constr c in + let t = EConstr.Unsafe.to_constr t in + let v = Vmsymtable.val_of_constr env (Evd.existential_opt_value0 sigma) c in EConstr.of_constr (nf_val env sigma v t) let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = |