diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 6 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 9 |
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 |