Fix #8119: anomalies in vm_compute with let and evars.

There were actually two broken things with VM + evars, the fixes are:
- Do not pass let-bound arguments to evars.
- Use the right order for evar arguments.

Native compilation seems to be suffering from the same shortcomings, I will
open a separate bug and adapt the PR.

1 files changed, 3 insertions, 0 deletions

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c944080503..255707dc7b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -209,6 +209,9 @@ and nf_evar env sigma evk stk =
   | Zapp args :: stk ->
     (** We assume that there is no consecutive Zapp nodes in a VM stack. Is that
         really an invariant? *)
+    (** Let-bound arguments are present in the evar arguments but not in the
+        type, so we turn the let into a product. *)
+    let hyps = Context.Named.drop_bodies hyps in
     let fold accu d = Term.mkNamedProd_or_LetIn d accu in
     let t = List.fold_left fold concl hyps in
     let t, args = nf_args env sigma args t in