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.

2 files changed, 3 insertions, 3 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 92d56d2904..182493baf9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1211,7 +1211,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 c79aca3d3c..71eef1a135 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