From 1b378d6b5625614189eee4d2817fe11ba6751f65 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 23 Jul 2018 18:34:52 +0200
Subject: Fix #8121: anomalies in native_compute with let and evars.

Même causes, mêmes effets, similar fix to #8119:
- Do not pass let-bound arguments to evars.

We seize the opportunity to remove the useless type information for Aevar.

Special fixes to native compilation:
- Evars are not handled correctly when iterating over lambda terms.
- Names.id_of_string is gone.
- Evar instances are not reified in the right order.
---
 kernel/nativeinstr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativeinstr.mli')

diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index 5075bd3d14..2d8e2ba2f0 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -25,7 +25,7 @@ and lambda =
   | Lrel          of Name.t * int 
   | Lvar          of Id.t
   | Lmeta         of metavariable * lambda (* type *)
-  | Levar         of Evar.t * lambda (* type *) * lambda array (* arguments *)
+  | Levar         of Evar.t * lambda array (* arguments *)
   | Lprod         of lambda * lambda 
   | Llam          of Name.t array * lambda  
   | Llet          of Name.t * lambda * lambda
-- 
cgit v1.2.3