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/nativeconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativeconv.ml')

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 931b8bbc86..c75dde843e 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -64,7 +64,7 @@ and conv_atom env pb lvl a1 a2 cu =
     match a1, a2 with
     | Ameta (m1,_), Ameta (m2,_) ->
       if Int.equal m1 m2 then cu else raise NotConvertible
-    | Aevar (ev1,_,args1), Aevar (ev2,_,args2) ->
+    | Aevar (ev1, args1), Aevar (ev2, args2) ->
       if Evar.equal ev1 ev2 then
         Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu
       else raise NotConvertible
-- 
cgit v1.2.3