aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/extratactics.ml44
-rw-r--r--tactics/hipattern.ml46
-rw-r--r--tactics/refine.ml6
-rw-r--r--tactics/rewrite.ml429
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tactics.ml14
7 files changed, 29 insertions, 34 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index fd5fbe25a..02d99d707 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -489,7 +489,7 @@ let unfold_head env (ids, csts) c =
| true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args))
| false, _ ->
let done_, args' =
- array_fold_left_i (fun i (done_, acc) arg ->
+ Array.fold_left_i (fun i (done_, acc) arg ->
if done_ then done_, arg :: acc
else match aux arg with
| true, arg' -> true, arg' :: acc
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index bf29d393e..7f0e486ab 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -754,9 +754,9 @@ let rec has_evar x =
| Fix ((_, tr)) | CoFix ((_, tr)) ->
has_evar_prec tr
and has_evar_array x =
- array_exists has_evar x
+ Array.exists has_evar x
and has_evar_prec (_, ts1, ts2) =
- array_exists has_evar ts1 || array_exists has_evar ts2
+ Array.exists has_evar ts1 || Array.exists has_evar ts2
TACTIC EXTEND has_evar
| [ "has_evar" constr(x) ] ->
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index bb35cedea..237c63a83 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -144,7 +144,7 @@ let is_tuple t =
"Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
let test_strict_disjunction n lc =
- array_for_all_i (fun i c ->
+ Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [_,None,c] -> isRel c && destRel c = (n - i)
| _ -> false) 0 lc
@@ -155,7 +155,7 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) t =
| Ind ind ->
let car = mis_constr_nargs ind in
let (mib,mip) = Global.lookup_inductive ind in
- if array_for_all (fun ar -> ar = 1) car
+ if Array.for_all (fun ar -> ar = 1) car
&& not (mis_is_recursive (ind,mib,mip))
&& (mip.mind_nrealargs = 0)
then
@@ -316,7 +316,7 @@ let match_with_nodep_ind t =
let (mib,mip) = Global.lookup_inductive ind in
if Array.length (mib.mind_packets)>1 then None else
let nodep_constr = has_nodep_prod_after mib.mind_nparams in
- if array_for_all nodep_constr mip.mind_nf_lc then
+ if Array.for_all nodep_constr mip.mind_nf_lc then
let params=
if mip.mind_nrealargs=0 then args else
fst (List.chop mib.mind_nparams args) in
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 1cb4f01e2..de073b5c9 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -115,7 +115,7 @@ let replace_by_meta env sigma = function
exception NoMeta
let replace_in_array keep_length env sigma a =
- if array_for_all (function (TH (_,_,[])) -> true | _ -> false) a then
+ if Array.for_all (function (TH (_,_,[])) -> true | _ -> false) a then
raise NoMeta;
let a' = Array.map (function
| (TH (c,mm,[])) when not keep_length -> c,mm,[]
@@ -347,7 +347,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
| Name id -> id
| _ -> error "Recursive functions must have names."
in
- let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
+ let fixes = Array.map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
let firsts,lasts = List.chop j (Array.to_list fixes) in
tclTHENS
(tclTHEN
@@ -364,7 +364,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
| Name id -> id
| _ -> error "Recursive functions must have names."
in
- let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
+ let cofixes = Array.map2 (fun f c -> (out_name f,c)) fi ai in
let firsts,lasts = List.chop j (Array.to_list cofixes) in
tclTHENS
(mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index c36ab2f83..fe869c340 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -121,7 +121,7 @@ let is_applied_rewrite_relation env sigma rels t =
if eq_constr (Lazy.force coq_eq) head then None
else
(try
- let params, args = array_chop (Array.length args - 2) args in
+ let params, args = Array.chop (Array.length args - 2) args in
let env' = Environ.push_rel_context rels env in
let evd, evar = Evarutil.new_evar sigma env' (new_Type ()) in
let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in
@@ -209,12 +209,6 @@ let get_transitive_proof env = find_class_proof transitive_type transitive_proof
exception FoundInt of int
-let array_find (arr: 'a array) (pred: int -> 'a -> bool): int =
- try
- for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (FoundInt i) done;
- raise Not_found
- with FoundInt i -> i
-
type hypinfo = {
cl : clausenv;
prf : constr;
@@ -239,7 +233,7 @@ let rec decompose_app_rel env evd t =
match kind_of_term t with
| App (f, args) ->
if Array.length args > 1 then
- let fargs, args = array_chop (Array.length args - 2) args in
+ let fargs, args = Array.chop (Array.length args - 2) args in
mkApp (f, fargs), args
else
let (f', args) = decompose_app_rel env evd args.(0) in
@@ -587,10 +581,11 @@ let resolve_subrelation env avoid car rel prf rel' res =
let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars =
let evars, morph_instance, proj, sigargs, m', args, args' =
- let first = try (array_find args' (fun i b -> b <> None))
- with Not_found -> raise (Invalid_argument "resolve_morphism") in
- let morphargs, morphobjs = array_chop first args in
- let morphargs', morphobjs' = array_chop first args' in
+ let first = match (Array.find_i (fun _ b -> b <> None) args') with
+ | Some i -> i
+ | None -> raise (Invalid_argument "resolve_morphism") in
+ let morphargs, morphobjs = Array.chop first args in
+ let morphargs', morphobjs' = Array.chop first args' in
let appm = mkApp(m, morphargs) in
let appmtype = Typing.type_of env (goalevars evars) appm in
let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') in
@@ -609,7 +604,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars
evars, morph, morph, sigargs, appm, morphobjs, morphobjs'
in
let projargs, subst, evars, respars, typeargs =
- array_fold_left2
+ Array.fold_left2
(fun (acc, subst, evars, sigargs, typeargs') x y ->
let (carrier, relation), sigargs = split_head sigargs in
match relation with
@@ -767,7 +762,7 @@ let subterm all flags (s : strategy) : strategy =
| Some false -> Some None
| Some true ->
let args' = Array.of_list (List.rev args') in
- if array_exists
+ if Array.exists
(function
| None -> false
| Some r -> not (is_rew_cast r.rew_prf)) args'
@@ -778,7 +773,7 @@ let subterm all flags (s : strategy) : strategy =
rew_evars = evars' }
in Some (Some res)
else
- let args' = array_map2
+ let args' = Array.map2
(fun aorig anew ->
match anew with None -> aorig
| Some r -> r.rew_to) args args'
@@ -887,7 +882,7 @@ let subterm all flags (s : strategy) : strategy =
let res = make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r in
Some (Some (coerce env avoid cstr res))
| x ->
- if array_for_all ((=) 0) ci.ci_cstr_ndecls then
+ if Array.for_all ((=) 0) ci.ci_cstr_ndecls then
let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in
let found, brs' = Array.fold_left
(fun (found, acc) br ->
@@ -1765,7 +1760,7 @@ let declare_projection n instance_id r =
let init =
match kind_of_term typ with
App (f, args) when eq_constr f (Lazy.force respectful) ->
- mkApp (f, fst (array_chop (Array.length args - 2) args))
+ mkApp (f, fst (Array.chop (Array.length args - 2) args))
| _ -> typ
in aux init
in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f88530eec..637269a66 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -211,7 +211,7 @@ let compute_construtor_signatures isrec (_,k as ity) =
let lc =
Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in
let lrecargs = dest_subterms mip.mind_recargs in
- array_map2 analrec lc lrecargs
+ Array.map2 analrec lc lrecargs
let elimination_sort_of_goal gl =
pf_apply Retyping.get_sort_family_of gl (pf_concl gl)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b1a9c6732..8e6fc8597 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -718,7 +718,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c
let last_arg c = match kind_of_term c with
| App (f,cl) ->
- array_last cl
+ Array.last cl
| _ -> anomaly "last_arg"
let nth_arg i c =
@@ -1305,7 +1305,7 @@ let intro_or_and_pattern loc b ll l' tac id gl =
check_or_and_pattern_size loc ll (Array.length nv);
tclTHENLASTn
(tclTHEN (simplest_case c) (clear [id]))
- (array_map2 (fun n l -> tac ((adjust_names_length n n l)@l'))
+ (Array.map2 (fun n l -> tac ((adjust_names_length n n l)@l'))
nv (Array.of_list ll))
gl
@@ -2315,7 +2315,7 @@ let ids_of_constr ?(all=false) vars c =
| Construct (ind,_)
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
- array_fold_left_from
+ Array.fold_left_from
(if all then 0 else mib.Declarations.mind_nparams)
aux vars args
| _ -> fold_constr aux vars c)
@@ -2328,7 +2328,7 @@ let decompose_indapp f args =
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
let first = mib.Declarations.mind_nparams_rec in
- let pars, args = array_chop first args in
+ let pars, args = Array.chop first args in
mkApp (f, pars), args
| _ -> f, args
@@ -2459,10 +2459,10 @@ let abstract_args gl generalize_vars dep id defined f args =
let parvars = ids_of_constr ~all:true Idset.empty f' in
if not (linear parvars args') then true, f, args
else
- match array_find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with
+ match Array.find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with
| None -> false, f', args'
| Some nonvar ->
- let before, after = array_chop nonvar args' in
+ let before, after = Array.chop nonvar args' in
true, mkApp (f', before), after
in
if dogen then
@@ -2941,7 +2941,7 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t
(tclTHEN
(induct_tac elim)
(tclMAP (fun id -> tclTRY (expand_hyp id)) (List.rev indhyps)))
- (array_map2 (induct_discharge destopt avoid tac) indsign names) gl
+ (Array.map2 (induct_discharge destopt avoid tac) indsign names) gl
(* Apply induction "in place" taking into account dependent
hypotheses from the context *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 02:21:46 +0000