Merge PR #11896: Use lists instead of arrays in evar instances.

Ack-by: SkySkimmer
Reviewed-by: maximedenes

14 files changed, 64 insertions, 56 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index f816599a17..b39ec37cd1 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -446,7 +446,7 @@ let rec norm_head info env t stack =
           Some c -> norm_head info env c stack
         | None ->
           let e, xs = ev in
-          let xs' = Array.map (apply_env env) xs in
+          let xs' = List.map (apply_env env) xs in
           (VAL(0, mkEvar (e,xs')), stack))
 
   (* non-neutral cases *)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index f85635528d..25aa8915ba 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -404,7 +404,7 @@ let matches_core env sigma allow_bound_rels
           Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2
 
       | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
-         Array.fold_left2 (sorec ctx env) subst args1 args2
+         List.fold_left2 (sorec ctx env) subst args1 args2
       | PInt i1, Int i2 when Uint63.equal i1 i2 -> subst
       | PFloat f1, Float f2 when Float64.equal f1 f2 -> subst
       | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 857918c928..ff278baf9f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -790,7 +790,7 @@ and detype_r d flags avoid env sigma t =
           id,l
         with Not_found ->
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
-          (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl)
+          (List.map (fun c -> (Id.of_string "__",c)) cl)
       in
         GEvar (id,
                List.map (on_snd (detype d flags avoid env sigma)) l)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3d887e1a95..f1506f5f59 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -195,7 +195,7 @@ let occur_rigidly flags env evd (evk,_) t =
     | Evar (evk',l as ev) ->
       if Evar.equal evk evk' then Rigid true
       else if is_frozen flags ev then
-        Rigid (Array.exists (fun x -> rigid_normal_occ (aux x)) l)
+        Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l)
       else Reducible
     | Cast (p, _, _) -> aux p
     | Lambda (na, t, b) -> aux b
@@ -351,6 +351,14 @@ let ise_array2 evd f v1 v2 =
   if Int.equal lv1 (Array.length v2) then allrec evd (pred lv1)
   else UnifFailure (evd,NotSameArgSize)
 
+let rec ise_inst2 evd f l1 l2 = match l1, l2 with
+| [], [] -> Success evd
+| [], (_ :: _) | (_ :: _), [] -> assert false
+| c1 :: l1, c2 :: l2 ->
+  match ise_inst2 evd f l1 l2 with
+  | Success evd' -> f evd' c1 c2
+  | UnifFailure _ as x -> x
+
 (* Applicative node of stack are read from the outermost to the innermost
    but are unified the other way. *)
 let rec ise_app_stack2 env f evd sk1 sk2 =
@@ -1019,7 +1027,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           if Evar.equal sp1 sp2 then
             match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with
             |None, Success i' ->
-              ise_array2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2
+              ise_inst2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2
             |_, (UnifFailure _ as x) -> x
             |Some _, _ -> UnifFailure (evd,NotSameArgSize)
           else UnifFailure (evd,NotSameHead)
@@ -1241,6 +1249,7 @@ let filter_possible_projections evd c ty ctxt args =
   (* Since args in the types will be replaced by holes, we count the
      fv of args to have a well-typed filter; don't know how necessary
     it is however to have a well-typed filter here *)
+  let args = Array.of_list args in
   let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in
   let fv2 = collect_vars evd (mkApp (c,args)) in
   let len = Array.length args in
@@ -1309,8 +1318,8 @@ let thin_evars env sigma sign c =
     match kind !sigma t with
     | Evar (ev, args) ->
        let evi = Evd.find_undefined !sigma ev in
-       let filter = Array.map (fun c -> Id.Set.subset (collect_vars !sigma c) ctx) args in
-       let filter = Filter.make (Array.to_list filter) in
+       let filter = List.map (fun c -> Id.Set.subset (collect_vars !sigma c) ctx) args in
+       let filter = Filter.make filter in
        let candidates = Option.map (List.map EConstr.of_constr) (evar_candidates evi) in
        let evd, ev = restrict_evar !sigma ev filter candidates in
        sigma := evd; whd_evar !sigma t
@@ -1336,9 +1345,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   if debug_ho_unification () then
     (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs);
      Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar));
-  let args = Array.map (nf_evar evd) args in
+  let args = List.map (nf_evar evd) args in
   let vars = List.map NamedDecl.get_id ctxt in
-  let argsubst = List.map2 (fun id c -> (id, c)) vars (Array.to_list args) in
+  let argsubst = List.map2 (fun id c -> (id, c)) vars args in
   let instance = List.map mkVar vars in
   let rhs = nf_evar evd rhs in
   if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd);
@@ -1416,7 +1425,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
      set_holes env_rhs' evd rhs' subst
   | [] -> evd, rhs in
 
-  let subst = make_subst (ctxt,Array.to_list args,argoccs) in
+  let subst = make_subst (ctxt,args,argoccs) in
 
   let evd, rhs' = set_holes env_rhs evd rhs subst in
   let rhs' = nf_evar evd rhs' in
@@ -1533,7 +1542,7 @@ let default_evar_selection flags evd (ev,args) =
       in spec :: aux args abs
     | l, [] -> List.map (fun _ -> default_occurrence_selection) l
     | [], _ :: _ -> assert false
-  in aux (Array.to_list args) evi.evar_abstract_arguments
+  in aux args evi.evar_abstract_arguments
 
 let second_order_matching_with_args flags env evd with_ho pbty ev l t =
   if with_ho then
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 50187d82cc..71edcaa231 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -113,7 +113,7 @@ let define_evar_as_product env evd (evk,args) =
   (* Quick way to compute the instantiation of evk with args *)
   let na,dom,rng = destProd evd prod in
   let evdom = mkEvar (fst (destEvar evd dom), args) in
-  let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
+  let evrngargs = mkRel 1 :: List.map (lift 1) args in
   let evrng =  mkEvar (fst (destEvar evd rng), evrngargs) in
   evd, mkProd (na, evdom, evrng)
 
@@ -152,7 +152,7 @@ let define_evar_as_lambda env evd (evk,args) =
   let evd,lam = define_pure_evar_as_lambda env evd evk in
   (* Quick way to compute the instantiation of evk with args *)
   let na,dom,body = destLambda evd lam in
-  let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
+  let evbodyargs = mkRel 1 :: List.map (lift 1) args in
   let evbody = mkEvar (fst (destEvar evd body), evbodyargs) in
   evd, mkLambda (na, dom, evbody)
 
@@ -163,7 +163,7 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function
       let evd,lam = define_pure_evar_as_lambda env evd evk in
       let _,_,body = destLambda evd lam in
       let evk = fst (destEvar evd body) in
-      evar_absorb_arguments env evd (evk, Array.cons a args) l
+      evar_absorb_arguments env evd (evk, a :: args) l
 
 (* Refining an evar to a sort *)
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index e475e4c52b..34684e4a34 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -217,7 +217,7 @@ type 'a update =
 | NoUpdate
 
 open Context.Named.Declaration
-let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign
+let inst_of_vars sign = List.map (get_id %> mkVar) sign
 
 let restrict_evar_key evd evk filter candidates =
   match filter, candidates with
@@ -247,7 +247,7 @@ let restrict_applied_evar evd (evk,argsv) filter candidates =
   | Some filter ->
       let evi = Evd.find evd evk in
       let subfilter = Filter.compose (evar_filter evi) filter in
-      Filter.filter_array subfilter argsv in
+      Filter.filter_list subfilter argsv in
   evd,(newevk,newargsv)
 
 (* Restrict an evar in the current evar_map *)
@@ -258,7 +258,7 @@ let restrict_evar evd evk filter candidates =
 let restrict_instance evd evk filter argsv =
   match filter with None -> argsv | Some filter ->
   let evi = Evd.find evd evk in
-  Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv
+  Filter.filter_list (Filter.compose (evar_filter evi) filter) argsv
 
 open Context.Rel.Declaration
 let noccur_evar env evd evk c =
@@ -269,7 +269,7 @@ let noccur_evar env evd evk c =
     if Evar.equal evk evk' then raise Occur
     else (if check_types then
             occur_rec false acc (existential_type evd ev');
-          Array.iter (occur_rec check_types acc) args')
+          List.iter (occur_rec check_types acc) args')
   | Rel i when i > k ->
      if not (Int.Set.mem (i-k) !cache) then
        let decl = Environ.lookup_rel i env in
@@ -552,17 +552,13 @@ let get_actual_deps env evd aliases l t =
 open Context.Named.Declaration
 let remove_instance_local_defs evd evk args =
   let evi = Evd.find evd evk in
-  let len = Array.length args in
-  let rec aux sign i = match sign with
-  | [] ->
-    let () = assert (i = len) in []
-  | LocalAssum _ :: sign ->
-    let () = assert (i < len) in
-    (Array.unsafe_get args i) :: aux sign (succ i)
-  | LocalDef _ :: sign ->
-    aux sign (succ i)
+  let rec aux sign args = match sign, args with
+  | [], [] -> []
+  | LocalAssum _ :: sign, c :: args -> c :: aux sign args
+  | LocalDef _ :: sign, _ :: args -> aux sign args
+  | _ -> assert false
   in
-  aux (evar_filtered_context evi) 0
+  aux (evar_filtered_context evi) args
 
 (* Check if an applied evar "?X[args] l" is a Miller's pattern *)
 
@@ -688,7 +684,7 @@ let make_projectable_subst aliases sigma evi args =
                 let all = Int.Map.add i [a, id] all in
                 (rest,all,cstrs,revmap))
         | _ -> anomaly (Pp.str "Instance does not match its signature.")) 0
-      sign (Array.rev_to_list args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in
+      sign (List.rev args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in
   (full_subst,cstr_subst)
 
 (*------------------------------------*
@@ -765,7 +761,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
        (mkRel 1)::(List.map (lift 1) inst_in_sign),
        push_rel d env,evd,Id.Set.add id.binder_name avoid))
       rel_sign
-      (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid)
+      (sign1,filter1,args1,inst_in_sign,env1,evd,avoid)
   in
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
@@ -775,11 +771,12 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let (evd, ev2_in_sign) =
     new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
-  let ev2_in_env = (fst (destEvar evd ev2_in_sign), Array.of_list inst2_in_env) in
+  let ev2_in_env = (fst (destEvar evd ev2_in_sign), inst2_in_env) in
   (evd, ev2_in_sign, ev2_in_env)
 
 let restrict_upon_filter evd evk p args =
   let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
+  let args = Array.of_list args in
   let len = Array.length args in
   Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i))
 
@@ -1034,7 +1031,7 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
     let p = invert_arg fullenv evd aliases k evk subst arg in
     extract_unique_projection p
   in
-  Array.map invert args'
+  List.map invert args'
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
  * variables) such that c becomes closed.
@@ -1390,9 +1387,9 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 =
     try evdref := Evd.add_universe_constraints !evdref cstr; true
     with UniversesDiffer -> false
   in
-  if Array.equal eq_constr argsv1 argsv2 then !evdref else
+  if List.equal eq_constr argsv1 argsv2 then !evdref else
   (* Filter and restrict if needed *)
-  let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
+  let args = List.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
   let untypedfilter =
     restrict_upon_filter evd evk
       (fun (a1,a2) -> unify flags TermUnification env evd Reduction.CONV a1 a2) args in
@@ -1452,7 +1449,7 @@ let occur_evar_upto_types sigma n c =
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
     | Evar (sp,args as e) ->
        if Evar.Set.mem sp !seen then
-         Array.iter occur_rec args
+         List.iter occur_rec args
        else (
          seen := Evar.Set.add sp !seen;
          Option.iter occur_rec (existential_opt_value0 sigma e);
@@ -1570,7 +1567,7 @@ let rec invert_definition unify flags choose imitate_defs
         (* Evar/Evar problem (but left evar is virtual) *)
         let aliases = lift_aliases k aliases in
         (try
-          let ev = (evk,Array.map (lift k) argsv) in
+          let ev = (evk,List.map (lift k) argsv) in
           let evd,body = project_evar_on_evar false unify flags env' !evdref aliases k None ev' ev in
           evdref := evd;
           body
@@ -1648,7 +1645,7 @@ let rec invert_definition unify flags choose imitate_defs
       | [], [] -> true
       | _ -> false
     in
-      is_id_subst filter_ctxt (Array.to_list argsv) &&
+      is_id_subst filter_ctxt argsv &&
       closed0 evd rhs &&
       Id.Set.subset (collect_vars evd rhs) !names
   in
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 0a1b731e6b..3fb80432ad 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -99,7 +99,7 @@ val refresh_universes :
   env -> evar_map -> types -> evar_map * types
 
 val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> env ->  evar_map ->
-  bool option -> Evar.t -> constr array -> constr array -> evar_map
+  bool option -> Evar.t -> constr list -> constr list -> evar_map
 
 val solve_evar_evar : ?force:bool ->
   (env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
@@ -128,7 +128,7 @@ val check_evar_instance : unifier -> unify_flags ->
   env -> evar_map -> Evar.t -> constr -> evar_map
 
 val remove_instance_local_defs :
-  evar_map -> Evar.t -> 'a array -> 'a list
+  evar_map -> Evar.t -> 'a list -> 'a list
 
 val get_type_of_refresh :
   ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 34498458a4..d672ddc906 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -423,8 +423,8 @@ and nf_evar env sigma evk args =
   let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
   let ty = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in
   if List.is_empty hyps then begin
-    assert (Int.equal (Array.length args) 0);
-    mkEvar (evk, [||]), ty
+    assert (Array.is_empty args);
+    mkEvar (evk, []), ty
   end
   else
     (* Let-bound arguments are present in the evar arguments but not
@@ -436,7 +436,7 @@ and nf_evar env sigma evk args =
     (* 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
+    mkEvar (evk, List.rev args), ty
 
 let evars_of_evar_map sigma =
   { Nativelambda.evars_val = Evd.existential_opt_value0 sigma;
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 3f2e690da5..1dfb8b2cd1 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -24,7 +24,7 @@ type case_info_pattern =
 type constr_pattern =
   | PRef of GlobRef.t
   | PVar of Id.t
-  | PEvar of Evar.t * constr_pattern array
+  | PEvar of constr_pattern Constr.pexistential
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of patvar * constr_pattern list
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b8635d03b7..6d30e0338e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -31,7 +31,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PRef r1, PRef r2 -> GlobRef.equal r1 r2
 | PVar v1, PVar v2 -> Id.equal v1 v2
 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) ->
-  Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2
+  Evar.equal ev1 ev2 && List.equal constr_pattern_eq ctx1 ctx2
 | PRel i1, PRel i2 ->
   Int.equal i1 i2
 | PApp (t1, arg1), PApp (t2, arg2) ->
@@ -115,7 +115,7 @@ let rec occurn_pattern n = function
       (occurn_pattern n c) ||
       (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
   | PMeta _ | PSoApp _ -> true
-  | PEvar (_,args) -> Array.exists (occurn_pattern n) args
+  | PEvar (_,args) -> List.exists (occurn_pattern n) args
   | PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ -> false
   | PFix (_,(_,tl,bl)) ->
      Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
@@ -190,7 +190,7 @@ let pattern_of_constr env sigma t =
         (* These are the two evar kinds used for existing goals *)
         (* see Proofview.mark_in_evm *)
          if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value0 sigma ev)
-         else PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+         else PEvar (evk,List.map (pattern_of_constr env) ctxt)
       | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
       | _ ->
          PMeta None)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 940150b15a..f7e3d651ff 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -607,7 +607,7 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk
     ((id,c)::subst, update, sigma) in
   let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in
   check_instance loc subst inst;
-  sigma, Array.map_of_list snd subst
+  sigma, List.map snd subst
 
 module Default =
 struct
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 70605d58ab..2c717b8774 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -86,7 +86,7 @@ let evaluable_reference_eq sigma r1 r2 = match r1, r2 with
 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2
 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2
 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
-  Evar.equal e1 e2 && Array.equal (EConstr.eq_constr sigma) ctx1 ctx2
+  Evar.equal e1 e2 && List.equal (EConstr.eq_constr sigma) ctx1 ctx2
 | _ -> false
 
 let mkEvalRef ref u =
@@ -408,7 +408,7 @@ let substl_with_function subst sigma constr =
         let (sigma, evk) = Evarutil.new_pure_evar venv sigma dummy in
         evd := sigma;
         minargs := Evar.Map.add evk min !minargs;
-        Vars.lift k (mkEvar (evk, [|fx;ref|]))
+        Vars.lift k (mkEvar (evk, [fx; ref]))
       | (fx, None) -> Vars.lift k fx
     else mkRel (i - Array.length v)
   | _ ->
@@ -455,7 +455,7 @@ let substl_checking_arity env subst sigma c =
   (* we propagate the constraints: solved problems are substituted;
      the other ones are replaced by the function symbol *)
   let rec nf_fix c = match EConstr.kind sigma c with
-  | Evar (i,[|fx;f|]) when Evar.Map.mem i minargs ->
+  | Evar (i,[fx;f]) when Evar.Map.mem i minargs ->
     (* FIXME: find a less hackish way of doing this *)
     begin match EConstr.kind sigma' c with
     | Evar _ -> f
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e168f6d1b6..f5aaac315a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -76,7 +76,7 @@ let occur_meta_or_undefined_evar evd c =
     | Evar (ev,args) ->
         (match evar_body (Evd.find evd ev) with
         | Evar_defined c ->
-            occrec (EConstr.Unsafe.to_constr c); Array.iter occrec args
+            occrec (EConstr.Unsafe.to_constr c); List.iter occrec args
         | Evar_empty -> raise Occur)
     | _ -> Constr.iter occrec c
   in try occrec c; false with Occur | Not_found -> true
@@ -138,9 +138,9 @@ let abstract_list_all env evd typ c l =
         error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
   evd,(p,typp)
 
-let set_occurrences_of_last_arg args =
+let set_occurrences_of_last_arg n =
   Evarconv.AtOccurrences AllOccurrences ::
-    List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified Abstraction.Abstract) args)
+    List.tl (List.init n (fun _ -> Evarconv.Unspecified Abstraction.Abstract))
 
 let occurrence_test _ _ _ env sigma _ c1 c2 =
   match EConstr.eq_constr_universes env sigma c1 c2 with
@@ -153,7 +153,8 @@ let abstract_list_all_with_dependencies env evd typ c l =
   let (evd, ev) = new_evar env evd typ in
   let evd,ev' = evar_absorb_arguments env evd (destEvar evd ev) l in
   let n = List.length l in
-  let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
+  let () = assert (n <= List.length (snd ev')) in
+  let argoccs = set_occurrences_of_last_arg n in
   let evd,b =
     Evarconv.second_order_matching
       (Evarconv.default_flags_of TransparentState.empty)
@@ -623,7 +624,7 @@ let subst_defined_metas_evars sigma (bl,el) c =
       substrec (EConstr.Unsafe.to_constr (pi2 (List.find select bl)))
     | Evar (evk,args) ->
       let eq c1 c2 = Constr.equal c1 (EConstr.Unsafe.to_constr c2) in
-      let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.for_all2 eq args args' in
+      let select (_,(evk',args'),_) = Evar.equal evk evk' && List.for_all2 eq args args' in
       (try substrec (EConstr.Unsafe.to_constr (pi3 (List.find select el)))
        with Not_found -> Constr.map substrec c)
     | _ -> Constr.map substrec c
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index d4da93cc5b..37c34d55cf 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -205,7 +205,7 @@ and nf_evar env sigma evk stk =
   let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
   let concl = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in
   if List.is_empty hyps then
-    nf_stk env sigma (mkEvar (evk, [||])) concl stk
+    nf_stk env sigma (mkEvar (evk, [])) concl stk
   else match stk with
   | Zapp args :: stk ->
     (* We assume that there is no consecutive Zapp nodes in a VM stack. Is that
@@ -217,6 +217,7 @@ and nf_evar env sigma evk stk =
     let t = List.fold_left fold concl hyps in
     let t, args = nf_args env sigma args t in
     let inst, args = Array.chop (List.length hyps) args in
+    let inst = Array.to_list inst in
     let c = mkApp (mkEvar (evk, inst), args) in
     nf_stk env sigma c t stk
   | _ ->