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

Ack-by: SkySkimmer
Reviewed-by: maximedenes

2 files changed, 3 insertions, 3 deletions

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