From 2ff9efcf617318fdfec9966cf3690d1fc4e56da7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 23 Jul 2018 17:59:30 +0200
Subject: 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.
---
 pretyping/vnorm.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping')

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
-- 
cgit v1.2.3