Fix #17871 inconsistency with native_compute and primitive floats

The Array.of_list in Nativevalues.args_of_accu could result in an
OCaml double array when some argument was a primitive float, making
all other argument sometimes wrongfully appear as float themselves.

kernel/nativeconv.ml

@@ -70,7 +70,7 @@ and conv_accu env pb lvl k1 k2 cu =
     conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
   else
     let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
-    Array.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
+    List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
 
 and conv_atom env pb lvl a1 a2 cu =
   if a1 == a2 then cu

kernel/nativevalues.ml

@@ -225,7 +225,7 @@ let accu_nargs (k:accumulator) =
 
 let args_of_accu (k:accumulator) =
   let acc = (get_accu k).acc_arg in
-  (Obj.magic (Array.of_list acc) : t array)
+  (Obj.magic acc : t list)
 
 let mk_fix_accu rec_pos pos types bodies =
   mk_accu (Afix(types,bodies,rec_pos, pos))
@@ -246,7 +246,7 @@ let force_cofix (cofix : t) =
   match atom with
   | Acofix (typ, norm, pos, CofixLazy f) ->
     let args = args_of_accu accu in
-    let f = Array.fold_right (fun arg f -> apply f arg) args f in
+    let f = List.fold_right (fun arg f -> apply f arg) args f in
     let v = apply f (Obj.magic ()) in
     let () = set_atom_of_accu accu (Acofix (typ, norm, pos, CofixValue v)) in
       v

kernel/nativevalues.mli

@@ -117,7 +117,7 @@ val napply : t -> t array -> t
 
 val dummy_value : unit -> t
 val atom_of_accu : accumulator -> atom
-val args_of_accu : accumulator -> t array
+val args_of_accu : accumulator -> t list
 val accu_nargs : accumulator -> int
 
 val cast_accu : t -> accumulator

pretyping/nativenorm.ml

@@ -260,7 +260,7 @@ and nf_args env sigma args t =
     let c = nf_val env sigma arg dom in
     (subst1 c codom, c::l)
   in
-  let t,l = Array.fold_right aux args (t,[]) in
+  let t,l = List.fold_right aux args (t,[]) in
   t, List.rev l
 
 and nf_bargs env sigma b t =
@@ -406,7 +406,7 @@ and nf_evar env sigma evk args =
     let fold accu d = EConstr.mkNamedProd_or_LetIn sigma d accu in
     let t = List.fold_left fold ty hyps in
     let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
-    let ty, args = nf_args env sigma args t in
+    let ty, args = nf_args env sigma (Array.to_list args) t in
     (* 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 *)