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, 10 insertions, 6 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 5df41ef76a..246acfc92e 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -354,9 +354,8 @@ and nf_atom_type env sigma atom =
       let env = push_rel (LocalAssum (n,dom)) env in
       let codom,s2 = nf_type_sort env sigma (codom vn) in
       mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2
-  | Aevar(evk,ty,args) ->
-    let ty = nf_type env sigma ty in
-    nf_evar env sigma evk ty args
+  | Aevar(evk,args) ->
+    nf_evar env sigma evk args
   | Ameta(mv,ty) ->
      let ty = nf_type env sigma ty in
      mkMeta mv, ty
@@ -398,22 +397,27 @@ and  nf_predicate env sigma ind mip params v pT =
       mkLambda(name,dom,body)
     | _ -> nf_type env sigma v
 
-and nf_evar env sigma evk ty args =
+and nf_evar env sigma evk args =
   let evi = try Evd.find sigma evk with Not_found -> assert false in
   let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
+  let ty = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in
   if List.is_empty hyps then begin
     assert (Int.equal (Array.length args) 0);
     mkEvar (evk, [||]), ty
   end
   else
+    (** 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 ty hyps in
     let ty, args = nf_args env sigma args t in
-    mkEvar (evk, Array.of_list args), ty
+    (** nf_args takes arguments in the reverse order but produces them in the
+        correct one, so we have to reverse them again for the evar node *)
+    mkEvar (evk, Array.rev_of_list args), ty
 
 let evars_of_evar_map sigma =
   { Nativelambda.evars_val = Evd.existential_opt_value0 sigma;
-    Nativelambda.evars_typ = Evd.existential_type0 sigma;
     Nativelambda.evars_metas = Evd.meta_type0 sigma }
 
 (* fork perf process, return profiler's process id *)