Use lists instead of arrays in evar instances.

This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.

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 73be36d031..e0a9527293 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -812,7 +812,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 26bf02aa25..1b562d427c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -199,7 +199,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
@@ -355,6 +355,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 =
@@ -1023,7 +1031,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)
@@ -1245,6 +1253,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
@@ -1313,8 +1322,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
@@ -1340,9 +1349,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);
@@ -1420,7 +1429,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
@@ -1537,7 +1546,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 4eae0cf86c..63cc8c7581 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
@@ -561,17 +561,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 *)
 
@@ -697,7 +693,7 @@ let make_projectable_subst aliases sigma evi args =
                 let all = Int.Map.add i [a,normalize_alias_opt sigma aliases 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)
 
 (*------------------------------------*
@@ -774,7 +770,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
@@ -784,11 +780,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))
 
@@ -1043,7 +1040,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.
@@ -1399,9 +1396,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
@@ -1461,7 +1458,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);
@@ -1579,7 +1576,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
@@ -1657,7 +1654,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 f989dae4c9..c950854d8f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -428,8 +428,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
@@ -441,7 +441,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 015c26531a..870b96813d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -599,7 +599,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 90dde01915..11163d6ede 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -82,7 +82,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
@@ -144,9 +144,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
@@ -159,7 +159,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)
@@ -629,7 +630,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
   | _ ->