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.

1 files changed, 3 insertions, 3 deletions

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 91f6add1c3..3bf23f1468 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -63,7 +63,7 @@ type atom =
   | Acofixe of t array * t array * int * t
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
-  | Aevar of Evar.t * t * t array
+  | Aevar of Evar.t * t array
   | Aproj of (inductive * int) * accumulator
 
 let accumulate_tag = 0
@@ -135,8 +135,8 @@ let mk_prod_accu s dom codom =
 let mk_meta_accu mv ty =
   mk_accu (Ameta (mv,ty))
 
-let mk_evar_accu ev ty args =
-  mk_accu (Aevar (ev,ty,args))
+let mk_evar_accu ev args =
+  mk_accu (Aevar (ev, args))
 
 let mk_proj_accu kn c = 
   mk_accu (Aproj (kn,c))