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

Ack-by: SkySkimmer
Reviewed-by: maximedenes

40 files changed, 197 insertions, 148 deletions

diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
new file mode 100644
index 0000000000..cd6b408813
--- /dev/null
+++ b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
@@ -0,0 +1,24 @@
+if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then
+
+    coqhammer_CI_REF="evar-inst-list"
+    coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
+
+    elpi_CI_REF="evar-inst-list"
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    equations_CI_REF="evar-inst-list"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    metacoq_CI_REF="evar-inst-list"
+    metacoq_CI_GITURL=https://github.com/ppedrot/metacoq
+
+    mtac2_CI_REF="evar-inst-list"
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+    quickchick_CI_REF="evar-inst-list"
+    quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
+
+    unicoq_CI_REF="evar-inst-list"
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 542893ad0b..00050a89e1 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -287,7 +287,7 @@ let constr_display csr =
       "LetIn("^(name_display na)^","^(term_display b)^","
       ^(term_display t)^","^(term_display c)^")"
   | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
-  | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display l)^")"
+  | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display (Array.of_list l))^")"
   | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")"
   | Ind ((sp,i),u) ->
       "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")"
@@ -383,7 +383,7 @@ let print_pure_constr csr =
       Array.iter (fun x -> print_space (); box_display x) l;
       print_string ")"
   | Evar (e,l) -> print_string "Evar#"; print_int (Evar.repr e); print_string "{";
-      Array.iter (fun x -> print_space (); box_display x) l;
+      List.iter (fun x -> print_space (); box_display x) l;
       print_string"}"
   | Const (c,u) -> print_string "Cons(";
       sp_con_display c;
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 4508633858..ca681e58f8 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -355,7 +355,7 @@ let iter_with_full_binders sigma g f n c =
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
   | App (c,l) -> f n c; Array.Fun1.iter f n l
-  | Evar (_,l) -> Array.Fun1.iter f n l
+  | Evar (_,l) -> List.iter (fun c -> f n c) l
   | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
@@ -717,7 +717,7 @@ let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq
 let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e)
 
 let of_existential : Constr.existential -> existential =
-  let gen : type a b. (a,b) eq -> 'c * b array -> 'c * a array = fun Refl x -> x in
+  let gen : type a b. (a,b) eq -> 'c * b list -> 'c * a list = fun Refl x -> x in
   gen unsafe_eq
 
 let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index fdcdfe11f4..5fcadfcef7 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -200,7 +200,7 @@ let make_pure_subst evi args =
       match args with
         | a::rest -> (rest, (NamedDecl.get_id decl, a)::l)
         | _ -> anomaly (Pp.str "Instance does not match its signature."))
-    (evar_filtered_context evi) (Array.rev_to_list args,[]))
+    (evar_filtered_context evi) (List.rev args,[]))
 
 (*------------------------------------*
  * functional operations on evar sets *
@@ -448,7 +448,7 @@ let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?type
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
   let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
-  evd, mkEvar (newevk,Array.of_list instance)
+  evd, mkEvar (newevk, instance)
 
 let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
   let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
@@ -506,7 +506,7 @@ let generalize_evar_over_rels sigma (ev,args) =
   List.fold_left2
     (fun (c,inst as x) a d ->
       if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x)
-     (evi.evar_concl,[]) (Array.to_list args) sign
+     (evi.evar_concl,[]) args sign
 
 (************************************)
 (* Removing a dependency in an evar *)
@@ -594,7 +594,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
                   (* No dependency at all, we can keep this ev's context hyp *)
                     (ri, true::filter)
                   with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter))
-                ctxt (Array.to_list l) (Id.Map.empty,[]) in
+                ctxt l (Id.Map.empty,[]) in
             (* Check if some rid to clear in the context of ev has dependencies
                in the type of ev and adjust the source of the dependency *)
             let _nconcl =
@@ -736,7 +736,7 @@ let undefined_evars_of_term evd t =
     match EConstr.kind evd c with
       | Evar (n, l) ->
         let acc = Evar.Set.add n acc in
-        Array.fold_left evrec acc l
+        List.fold_left evrec acc l
       | _ -> EConstr.fold evd evrec acc c
   in
   evrec Evar.Set.empty t
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 1dec63aaf0..b5c7ccb283 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -88,7 +88,7 @@ val new_evar_instance :
  named_context_val -> evar_map -> types ->
   constr list -> evar_map * constr
 
-val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
+val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list
 
 val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 65fe261ff4..5642145f6d 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -233,32 +233,27 @@ exception NotInstantiatedEvar
 (* Note: let-in contributes to the instance *)
 
 let evar_instance_array test_id info args =
-  let len = Array.length args in
-  let rec instrec filter ctxt i = match filter, ctxt with
-  | [], [] ->
-    if Int.equal i len then []
-    else instance_mismatch ()
-  | false :: filter, _ :: ctxt ->
-    instrec filter ctxt i
-  | true :: filter, d :: ctxt ->
-    if i < len then
-      let c = Array.unsafe_get args i in
-      if test_id d c then instrec filter ctxt (succ i)
-      else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i)
-    else instance_mismatch ()
+  let rec instrec filter ctxt args = match filter, ctxt, args with
+  | [], [], [] -> []
+  | false :: filter, _ :: ctxt, args ->
+    instrec filter ctxt args
+  | true :: filter, d :: ctxt, c :: args ->
+    if test_id d c then instrec filter ctxt args
+    else (NamedDecl.get_id d, c) :: instrec filter ctxt args
   | _ -> instance_mismatch ()
   in
   match Filter.repr (evar_filter info) with
   | None ->
-     let map i d =
-      if (i < len) then
-        let c = Array.unsafe_get args i in
-        if test_id d c then None else Some (NamedDecl.get_id d, c)
-      else instance_mismatch ()
+    let rec instance ctxt args = match ctxt, args with
+    | [], [] -> []
+    | d :: ctxt, c :: args ->
+      if test_id d c then instance ctxt args
+      else (NamedDecl.get_id d, c) :: instance ctxt args
+    | _ -> instance_mismatch ()
     in
-    List.map_filter_i map (evar_context info)
+    instance (evar_context info) args
   | Some filter ->
-    instrec filter (evar_context info) 0
+    instrec filter (evar_context info) args
 
 let make_evar_instance_array info args =
   evar_instance_array (NamedDecl.get_id %> isVarId) info args
@@ -794,7 +789,7 @@ let restrict evk filter ?candidates ?src evd =
   | _ -> Evar.Set.add evk evd.last_mods in
   let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
+  let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
@@ -1405,7 +1400,7 @@ let evars_of_term evd c =
   let rec evrec acc c =
     let c = MiniEConstr.whd_evar evd c in
     match kind c with
-    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+    | Evar (n, l) -> Evar.Set.add n (List.fold_left evrec acc l)
     | _ -> Constr.fold evrec acc c
   in
   evrec Evar.Set.empty c
@@ -1413,7 +1408,7 @@ let evars_of_term evd c =
 let evar_nodes_of_term c =
   let rec evrec acc c =
     match kind c with
-    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+    | Evar (n, l) -> Evar.Set.add n (List.fold_left evrec acc l)
     | _ -> Constr.fold evrec acc c
   in
   evrec Evar.Set.empty c
diff --git a/engine/evd.mli b/engine/evd.mli
index bbdb63a467..c6c4a71b22 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -247,9 +247,9 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option
 val existential_opt_value0 : evar_map -> existential -> constr option
 
 val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info ->
-  'a array -> (Id.t * 'a) list
+  'a list -> (Id.t * 'a) list
 
-val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr
+val instantiate_evar_array : evar_info -> econstr -> econstr list -> econstr
 
 val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
   evar_map ->  evar_map -> evar_map
diff --git a/engine/termops.ml b/engine/termops.ml
index 16f2a87c1e..6d779e6a35 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -636,8 +636,8 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       if b' == b then c
       else mkProj (p, b')
   | Evar (e,al) ->
-    let al' = Array.map_left (f l) al in
-      if Array.for_all2 (==) al' al then c
+    let al' = List.map_left (f l) al in
+      if List.for_all2 (==) al' al then c
       else mkEvar (e, al')
   | Case (ci,p,b,bl) ->
       (* In v8 concrete syntax, predicate is after the term to match! *)
@@ -707,8 +707,8 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
       let c' = f l c in
         if c' == c then cstr else mkProj (p, c')
   | Evar (e,al) ->
-      let al' = Array.map (f l) al in
-      if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
+      let al' = List.map (f l) al in
+      if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
   | Case (ci,p,c,bl) when userview ->
       let p' = map_return_predicate_with_full_binders sigma g f l ci p in
       let c' = f l c in
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 6000650ad9..a691239ee2 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -131,7 +131,7 @@ let nf_evars_and_universes_opt_subst f subst =
   let rec aux c =
     match kind c with
     | Evar (evk, args) ->
-      let args = Array.map aux args in
+      let args = List.map aux args in
       (match try f (evk, args) with Not_found -> None with
       | None -> mkEvar (evk, args)
       | Some c -> aux c)
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c31cdae6f5..de02882370 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -613,7 +613,7 @@ let rec to_constr lfts v =
                     subst_constr subs f)
     | FEvar ((ev,args),env) ->
       let subs = comp_subs lfts env in
-        mkEvar(ev,Array.map (fun a -> subst_constr subs a) args)
+        mkEvar(ev,List.map (fun a -> subst_constr subs a) args)
     | FLIFT (k,a) -> to_constr (el_shft k lfts) a
 
     | FInt i ->
@@ -1408,7 +1408,7 @@ and norm_head info tab m =
             Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
           mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
       | FEvar((i,args),env) ->
-          mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
+          mkEvar(i, List.map (fun a -> kl info tab (mk_clos env a)) args)
       | FProj (p,c) ->
           mkProj (p, kl info tab c)
       | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 8c7aa6b17a..65de52c0f6 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -670,7 +670,7 @@ let rec lambda_of_constr env c =
   match Constr.kind c with
   | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta")
   | Evar (evk, args) ->
-    let args = lambda_of_args env 0 args in
+    let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
     Levar (evk, args)
 
   | Cast (c, _, _) -> lambda_of_constr env c
@@ -799,9 +799,6 @@ and lambda_of_args env start args =
       (fun i -> lambda_of_constr env args.(start + i))
   else empty_args
 
-
-
-
 (*********************************)
 let dump_lambda = ref false
 
diff --git a/kernel/constr.ml b/kernel/constr.ml
index ade03fdf93..703e3616a0 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -71,7 +71,7 @@ type case_info =
 
 (* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
-type 'constr pexistential = existential_key * 'constr array
+type 'constr pexistential = existential_key * 'constr list
 type ('constr, 'types) prec_declaration =
     Name.t binder_annot array * 'types array * 'constr array
 type ('constr, 'types) pfixpoint =
@@ -110,7 +110,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
 type t = (t, t, Sorts.t, Instance.t) kind_of_term
 type constr = t
 
-type existential = existential_key * constr array
+type existential = existential_key * constr list
 
 type types = constr
 
@@ -470,7 +470,7 @@ let fold f acc c = match kind c with
   | LetIn (_,b,t,c) -> f (f (f acc b) t) c
   | App (c,l) -> Array.fold_left f (f acc c) l
   | Proj (_p,c) -> f acc c
-  | Evar (_,l) -> Array.fold_left f acc l
+  | Evar (_,l) -> List.fold_left f acc l
   | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
   | Fix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
@@ -490,7 +490,7 @@ let iter f c = match kind c with
   | LetIn (_,b,t,c) -> f b; f t; f c
   | App (c,l) -> f c; Array.iter f l
   | Proj (_p,c) -> f c
-  | Evar (_,l) -> Array.iter f l
+  | Evar (_,l) -> List.iter f l
   | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
   | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
@@ -509,7 +509,7 @@ let iter_with_binders g f n c = match kind c with
   | Lambda (_,t,c) -> f n t; f (g n) c
   | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
   | App (c,l) -> f n c; Array.Fun1.iter f n l
-  | Evar (_,l) -> Array.Fun1.iter f n l
+  | Evar (_,l) -> List.iter (fun c -> f n c) l
   | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
   | Proj (_p,c) -> f n c
   | Fix (_,(_,tl,bl)) ->
@@ -536,7 +536,7 @@ let fold_constr_with_binders g f n acc c =
   | LetIn (_na,b,t,c) -> f (g  n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_p,c) -> f n acc c
-  | Evar (_,l) -> Array.fold_left (f n) acc l
+  | Evar (_,l) -> List.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(_,tl,bl)) ->
       let n' = iterate g (Array.length tl) n in
@@ -657,7 +657,7 @@ let map_gen userview f c = match kind c with
       if t' == t then c
       else mkProj (p, t')
   | Evar (e,l) ->
-      let l' = Array.Smart.map f l in
+      let l' = List.Smart.map f l in
       if l'==l then c
       else mkEvar (e, l')
   | Case (ci,p,b,bl) when userview ->
@@ -722,7 +722,8 @@ let fold_map f accu c = match kind c with
       if t' == t then accu, c
       else accu, mkProj (p, t')
   | Evar (e,l) ->
-      let accu, l' = Array.Smart.fold_left_map f accu l in
+    (* Doesn't matter, we should not hashcons evars anyways *)
+      let accu, l' = List.fold_left_map f accu l in
       if l'==l then accu, c
       else accu, mkEvar (e, l')
   | Case (ci,p,b,bl) ->
@@ -782,7 +783,7 @@ let map_with_binders g f l c0 = match kind c0 with
     if t' == t then c0
     else mkProj (p, t')
   | Evar (e, al) ->
-    let al' = Array.Fun1.Smart.map f l al in
+    let al' = List.Smart.map (fun c -> f l c) al in
     if al' == al then c0
     else mkEvar (e, al')
   | Case (ci, p, c, bl) ->
@@ -834,7 +835,7 @@ let fold_with_full_binders g f n acc c =
   | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_,c) -> f n acc c
-  | Evar (_,l) -> Array.fold_left (f n) acc l
+  | Evar (_,l) -> List.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
@@ -880,7 +881,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
     Int.equal len (Array.length l2) &&
     leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2
   | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2
-  | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2
+  | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2
   | Const (c1,u1), Const (c2,u2) ->
     (* The args length currently isn't used but may as well pass it. *)
     Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2
@@ -1039,7 +1040,7 @@ let constr_ord_int f t1 t2 =
     | Meta m1, Meta m2 -> Int.compare m1 m2
     | Meta _, _ -> -1 | _, Meta _ -> 1
     | Evar (e1,l1), Evar (e2,l2) ->
-        (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
+        (Evar.compare =? (List.compare f)) e1 e2 l1 l2
     | Evar _, _ -> -1 | _, Evar _ -> 1
     | Sort s1, Sort s2 -> Sorts.compare s1 s2
     | Sort _, _ -> -1 | _, Sort _ -> 1
@@ -1141,7 +1142,7 @@ let hasheq t1 t2 =
       n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2
     | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2
     | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2
-    | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2
+    | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && List.equal (==) l1 l2
     | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
     | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2
     | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2
@@ -1221,7 +1222,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
         let l, hl = hash_term_array l in
         (App (c,l), combinesmall 7 (combine hl hc))
       | Evar (e,l) ->
-        let l, hl = hash_term_array l in
+        let l, hl = hash_list_array l in
         (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
       | Const (c,u) ->
         let c' = sh_con c in
@@ -1289,6 +1290,14 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
     let h = !accu land 0x3FFFFFFF in
     (HashsetTermArray.repr h t term_array_table, h)
 
+  and hash_list_array l =
+    let fold accu c =
+      let c, h = sh_rec c in
+      (combine accu h, c)
+    in
+    let h, l = List.fold_left_map fold 0 l in
+    (l, h land 0x3FFFFFFF)
+
   in
   (* Make sure our statically allocated Rels (1 to 16) are considered
      as canonical, and hence hash-consed to themselves *)
@@ -1316,7 +1325,7 @@ let rec hash t =
     | App (c,l) ->
       combinesmall 7 (combine (hash_term_array l) (hash c))
     | Evar (e,l) ->
-      combinesmall 8 (combine (Evar.hash e) (hash_term_array l))
+      combinesmall 8 (combine (Evar.hash e) (hash_term_list l))
     | Const (c,u) ->
       combinesmall 9 (combine (Constant.hash c) (Instance.hash u))
     | Ind (ind,u) ->
@@ -1339,6 +1348,9 @@ let rec hash t =
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine acc (hash t)) 0 t
 
+and hash_term_list t =
+  List.fold_left (fun acc t -> combine (hash t) acc) 0 t
+
 module CaseinfoHash =
 struct
   type t = case_info
@@ -1458,7 +1470,7 @@ let rec debug_print c =
        prlist_with_sep spc debug_print (Array.to_list l) ++ str")")
   | Evar (e,l) -> hov 1
       (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
-       prlist_with_sep spc debug_print (Array.to_list l) ++str"}")
+       prlist_with_sep spc debug_print l ++str"}")
   | Const (c,u) -> str"Cst(" ++ pr_puniverses (Constant.debug_print c) u ++ str")"
   | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
   | Construct (((sp,i),j),u) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 16919b705a..00051d7551 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -83,7 +83,7 @@ val mkFloat : Float64.t -> constr
 val mkMeta : metavariable -> constr
 
 (** Constructs an existential variable *)
-type existential = Evar.t * constr array
+type existential = Evar.t * constr list
 val mkEvar : existential -> constr
 
 (** Construct a sort *)
@@ -203,9 +203,9 @@ val mkCoFix : cofixpoint -> constr
 
 (** {6 Concrete type for making pattern-matching. } *)
 
-(** [constr array] is an instance matching definitional [named_context] in
+(** [constr list] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
-type 'constr pexistential = Evar.t * 'constr array
+type 'constr pexistential = Evar.t * 'constr list
 
 type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Rel       of int                                  (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *)
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index f987164d52..662ad550b8 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
     end
   | FEvar ((_,args),e) ->
     let variances = infer_stack infos variances stk in
-    infer_vect infos variances (Array.map (mk_clos e) args)
+    infer_list infos variances (List.map (mk_clos e) args)
   | FRel _ -> infer_stack infos variances stk
   | FInt _ -> infer_stack infos variances stk
   | FFloat _ -> infer_stack infos variances stk
@@ -168,6 +168,9 @@ and infer_stack infos variances (stk:CClosure.stack) =
 and infer_vect infos variances v =
   Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
 
+and infer_list infos variances v =
+  List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
+
 let infer_term cv_pb env variances c =
   let open CClosure in
   let infos = (create_clos_infos all env, create_tab ()) in
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index aa513c1536..317141e324 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -405,7 +405,7 @@ let rec map_kn f f' c =
             if (ct'== ct && l'==l) then c
             else mkApp (ct',l')
       | Evar (e,l) ->
-          let l' = Array.Smart.map func l in
+          let l' = List.Smart.map func l in
             if (l'==l) then c
             else mkEvar (e,l')
       | Fix (ln,(lna,tl,bl)) ->
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 9ed0f6f411..02ee501f5f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -474,7 +474,7 @@ let rec lambda_of_constr cache env sigma c =
   | Evar (evk,args as ev) ->
      (match evar_value sigma ev with
      | None ->
-        let args = Array.map (lambda_of_constr cache env sigma) args in
+        let args = Array.map_of_list (fun c -> lambda_of_constr cache env sigma c) args in
         Levar(evk, args)
      | Some t -> lambda_of_constr cache env sigma t)
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7574d7b21e..4ff90dd70d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -367,9 +367,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let el1 = el_stack lft1 v1 in
           let el2 = el_stack lft2 v2 in
           let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
-          convert_vect l2r infos el1 el2
-            (Array.map (mk_clos env1) args1)
-            (Array.map (mk_clos env2) args2) cuniv
+          convert_list l2r infos el1 el2
+            (List.map (mk_clos env1) args1)
+            (List.map (mk_clos env2) args2) cuniv
         else raise NotConvertible
 
     (* 2 index known to be bound to no constant *)
@@ -702,6 +702,13 @@ and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv =
   in
   Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv
 
+and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
+| [], [] -> cuniv
+| c1 :: v1, c2 :: v2 ->
+  let cuniv = ccnv CONV l2r infos lft1 lft2 c1 c2 cuniv in
+  convert_list l2r infos lft1 lft2 v1 v2 cuniv
+| _, _ -> raise NotConvertible
+
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_clos_infos ~evars reds env in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 35e131020b..f002bbc57a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1559,7 +1559,7 @@ let assert_replacing id newt tac =
         if Id.equal n id then ev' else mkVar n
       in
       let (e, _) = destEvar sigma ev in
-      (sigma, mkEvar (e, Array.map_of_list map nc))
+      (sigma, mkEvar (e, List.map map nc))
     end
   end in
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e0b083a70a..134a9e4b36 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -537,7 +537,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) =
   let rec put evlist c = match Constr.kind c with
   | Evar (k, a) ->
     if List.mem_assoc k evlist || Evd.mem sigma0 k || List.mem k rigid then evlist else
-    let n = max 0 (Array.length a - nenv) in
+    let n = max 0 (List.length a - nenv) in
     let t = abs_evar n k in (k, (n, t)) :: put evlist t
   | _ -> Constr.fold put evlist c in
   let evlist = put [] c0 in
@@ -549,6 +549,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) =
   | Evar (ev, a) ->
     let j, n = lookup ev i evlist in
     if j = 0 then Constr.map (get i) c else if n = 0 then mkRel j else
+    let a = Array.of_list a in
     mkApp (mkRel j, Array.init n (fun k -> get i a.(n - 1 - k)))
   | _ -> Constr.map_with_binders ((+) 1) get i c in
   let rec loop c i = function
@@ -598,7 +599,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   let rec put evlist c = match Constr.kind c with
   | Evar (k, a) ->
     if List.mem_assoc k evlist || Evd.mem sigma0 k then evlist else
-    let n = max 0 (Array.length a - nenv) in
+    let n = max 0 (List.length a - nenv) in
     let k_ty =
       Retyping.get_sort_family_of
         (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in
@@ -636,6 +637,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   | Evar (ev, a) ->
     let j, n = lookup ev i evlist in
     if j = 0 then Constr.map (get evlist i) c else if n = 0 then mkRel j else
+    let a = Array.of_list a in
     mkApp (mkRel j, Array.init n (fun k -> get evlist i a.(n - 1 - k)))
   | _ -> Constr.map_with_binders ((+) 1) (get evlist) i c in
   let rec app extra_args i c = match decompose_app c with
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 1c776398e7..d5a781e472 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -263,7 +263,7 @@ let nf_open_term sigma0 ise c =
   let rec nf c' = match kind c' with
   | Evar ex ->
     begin try nf (existential_value0 s ex) with _ ->
-    let k, a = ex in let a' = Array.map nf a in
+    let k, a = ex in let a' = List.map nf a in
     if not (Evd.mem !s' k) then
       s' := Evd.add !s' k (Evarutil.nf_evar_info s (Evd.find s k));
     mkEvar (k, a')
@@ -307,7 +307,7 @@ let pf_unify_HO gl t1 t2 =
 
 (* This is what the definition of iter_constr should be... *)
 let iter_constr_LR f c = match kind c with
-  | Evar (k, a) -> Array.iter f a
+  | Evar (k, a) -> List.iter f a
   | Cast (cc, _, t) -> f cc; f t
   | Prod (_, t, b) | Lambda (_, t, b)  -> f t; f b
   | LetIn (_, v, t, b) -> f v; f t; f b
@@ -387,7 +387,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
     with NotInstantiatedEvar ->
     if Evd.mem sigma0 k then map put c else
     let evi = Evd.find !sigma k in
-    let dc = List.firstn (max 0 (Array.length a - nenv)) (evar_filtered_context evi) in
+    let dc = List.firstn (max 0 (List.length a - nenv)) (evar_filtered_context evi) in
     let abs_dc (d, c) = function
     | Context.Named.Declaration.LocalDef (x, b, t) ->
         d, mkNamedLetIn x (put b) (put t) c
@@ -601,7 +601,8 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
         | KpatFixed | KpatConst -> ise
         | KpatEvar _ ->
           let _, pka = destEvar u.up_f and _, ka = destEvar f in
-          unif_HO_args env ise pka 0 ka
+          let fold ise pk k = unif_HO env ise (EConstr.of_constr pk) (EConstr.of_constr k) in
+          List.fold_left2 fold ise pka ka
         | KpatLet ->
           let x, v, t, b = destLetIn f in
           let _, pv, _, pb = destLetIn u.up_f in
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
   | _ ->
diff --git a/proofs/goal.ml b/proofs/goal.ml
index b1f8fd3e97..53d3047bc7 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -69,7 +69,7 @@ module V82 = struct
     let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in
     let evars = Evd.restore_future_goals evars prev_future_goals in
     let ctxt = Environ.named_context_of_val hyps in
-    let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
+    let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in
     let ev = EConstr.mkEvar (evk,inst) in
     (evk, ev, evars)
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 57eab7ddf8..a51fc8b347 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1188,7 +1188,7 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
       with Refiner.FailError _ -> raise Not_found
   in
   let evd = sig_sig gls' in
-  let t' = mkEvar (ev, Array.of_list subst) in
+  let t' = mkEvar (ev, subst) in
   let term = Evarutil.nf_evar evd t' in
   term, evd
   end in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8c4400a80f..0df4f5b207 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2763,8 +2763,8 @@ let pose_tac na c =
       let id = make_annot id Sorts.Relevant in
       let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in
       let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in
-      let inst = Array.map_of_list (fun d -> mkVar (get_id d)) (named_context env) in
-      let body = mkEvar (ev, Array.append [|mkRel 1|] inst) in
+      let inst = List.map (fun d -> mkVar (get_id d)) (named_context env) in
+      let body = mkEvar (ev, mkRel 1 :: inst) in
       (sigma, mkLetIn (map_annot Name.mk_name id, c, t, body))
     end
   end
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 2102cd1172..e77040a8db 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -375,7 +375,7 @@ let () = define1 "constr_kind" constr begin fun c ->
   | Evar (evk, args) ->
     v_blk 3 [|
       Value.of_int (Evar.repr evk);
-      Value.of_array Value.of_constr args;
+      Value.of_array Value.of_constr (Array.of_list args);
     |]
   | Sort s ->
     v_blk 4 [|Value.of_ext Value.val_sort s|]
@@ -469,7 +469,7 @@ let () = define1 "constr_make" valexpr begin fun knd ->
   | (3, [|evk; args|]) ->
     let evk = Evar.unsafe_of_int (Value.to_int evk) in
     let args = Value.to_array Value.to_constr args in
-    EConstr.mkEvar (evk, args)
+    EConstr.mkEvar (evk, Array.to_list args)
   | (4, [|s|]) ->
     let s = Value.to_ext Value.val_sort s in
     EConstr.mkSort (EConstr.Unsafe.to_sorts s)
@@ -603,7 +603,7 @@ let () = define3 "constr_in_context" ident constr closure begin fun id t c ->
       thaw c >>= fun _ ->
       Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state (Proofview.Goal.goal gl)] >>= fun () ->
       let args = List.map (fun d -> EConstr.mkVar (get_id d)) (EConstr.named_context env) in
-      let args = Array.of_list (EConstr.mkRel 1 :: args) in
+      let args = EConstr.mkRel 1 :: args in
       let ans = EConstr.mkEvar (evk, args) in
       let ans = EConstr.mkLambda (Context.make_annot (Name id) Sorts.Relevant, t, ans) in
       return (Value.of_constr ans)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 5555a2c68e..fddc84b398 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -57,16 +57,16 @@ let contract3 env sigma a b c = match contract env sigma [a;b;c] with
 let contract4 env sigma a b c d = match contract env sigma [a;b;c;d] with
   | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false
 
-let contract1_vect env sigma a v =
-  match contract env sigma (a :: Array.to_list v) with
-  | env, a::l -> env,a,Array.of_list l
+let contract1 env sigma a v =
+  match contract env sigma (a :: v) with
+  | env, a::l -> env,a,l
   | _ -> assert false
 
 let rec contract3' env sigma a b c = function
   | OccurCheck (evk,d) ->
     let x,d = contract4 env sigma a b c d in x,OccurCheck(evk, d)
   | NotClean ((evk,args),env',d) ->
-      let env',d,args = contract1_vect env' sigma d args in
+      let env',d,args = contract1 env' sigma d args in
       contract3 env sigma a b c,NotClean((evk,args),env',d)
   | ConversionFailed (env',t1,t2) ->
       let (env',t1,t2) = contract2 env' sigma t1 t2 in
@@ -299,9 +299,9 @@ let explain_unification_error env sigma p1 p2 = function
         [str "cannot instantiate " ++ quote (pr_existential_key sigma evk)
         ++ strbrk " because " ++ pr_leconstr_env env sigma c ++
         strbrk " is not in its scope" ++
-        (if Array.is_empty args then mt() else
+        (if List.is_empty args then mt() else
          strbrk ": available arguments are " ++
-         pr_sequence (pr_leconstr_env env sigma) (List.rev (Array.to_list args)))]
+         pr_sequence (pr_leconstr_env env sigma) (List.rev args))]
      | NotSameArgSize | NotSameHead | NoCanonicalStructure ->
         (* Error speaks from itself *) []
      | ConversionFailed (env,t1,t2) ->
diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml
index c529972b8d..b8564037e0 100644
--- a/vernac/retrieveObl.ml
+++ b/vernac/retrieveObl.ml
@@ -72,7 +72,7 @@ let subst_evar_constr evm evs n idf t =
       *)
       let args =
         let n = match chop with None -> 0 | Some c -> c in
-        let l, r = CList.chop n (List.rev (Array.to_list args)) in
+        let l, r = CList.chop n (List.rev args) in
         List.rev r
       in
       let args =