From 45e14bdb854fe5da40c2ed1d9ca575ae8d435d36 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Sep 2018 18:55:30 +0200
Subject: 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.
---
 tactics/class_tactics.ml | 2 +-
 tactics/tactics.ml       | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3