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

Ack-by: SkySkimmer
Reviewed-by: maximedenes

3 files changed, 10 insertions, 7 deletions

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