Merge PR #13854: Normalize evars during bytecode compilation.

Reviewed-by: SkySkimmer
Ack-by: ppedrot
Ack-by: ejgallego

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 ();