From f89f0eb4717b64f10bdd0a0edc9e93b949bcb33d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 12 Feb 2021 18:11:52 +0100
Subject: 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.
---
 kernel/vmsymtable.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/vmsymtable.mli')

diff --git a/kernel/vmsymtable.mli b/kernel/vmsymtable.mli
index e480bfcec1..c6dc09d944 100644
--- a/kernel/vmsymtable.mli
+++ b/kernel/vmsymtable.mli
@@ -14,7 +14,7 @@ open Names
 open Constr
 open Environ
 
-val val_of_constr : env -> constr -> Vmvalues.values
+val val_of_constr : env -> (existential -> constr option) -> constr -> Vmvalues.values
 
 val set_opaque_const      : Constant.t -> unit
 val set_transparent_const : Constant.t -> unit
-- 
cgit v1.2.3