aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml10
-rw-r--r--plugins/funind/functional_principles_types.ml6
-rw-r--r--plugins/funind/glob_term_to_relation.ml18
-rw-r--r--plugins/funind/indfun.ml16
-rw-r--r--plugins/funind/invfun.ml10
-rw-r--r--plugins/funind/merge.ml4
-rw-r--r--plugins/funind/recdef.ml8
7 files changed, 36 insertions, 36 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8ea4be631c..0796930fca 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -93,7 +93,7 @@ let observe_tac s = observe_tac_stream (str s)
let list_chop ?(msg="") n l =
try
- list_chop n l
+ List.chop n l
with Failure (msg') ->
failwith (msg ^ msg')
@@ -319,7 +319,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
)
in
let new_type_of_hyp,ctxt_size,witness_fun =
- list_fold_left_i
+ List.fold_left_i
(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
try
let witness = Intmap.find i sub in
@@ -1168,7 +1168,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
typess
in
let pte_to_fix,rev_info =
- list_fold_left_i
+ List.fold_left_i
(fun i (acc_map,acc_info) (pte,_,_) ->
let infos = info_array.(i) in
let type_args,_ = decompose_prod infos.types in
@@ -1557,7 +1557,7 @@ let prove_principle_for_gen
(* str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
(* str "npost_rec_arg := " ++ int npost_rec_arg ); *)
let (post_rec_arg,pre_rec_arg) =
- Util.list_chop npost_rec_arg princ_info.args
+ Util.List.chop npost_rec_arg princ_info.args
in
let rec_arg_id =
match List.rev post_rec_arg with
@@ -1624,7 +1624,7 @@ let prove_principle_for_gen
Elim.h_decompose_and (mkVar hid);
(fun g ->
let new_hyps = pf_ids_of_hyps g in
- tcc_list := List.rev (list_subtract new_hyps (hid::hyps));
+ tcc_list := List.rev (List.subtract new_hyps (hid::hyps));
if !tcc_list = []
then
begin
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e2dc149b09..f2eb4b23cf 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -88,7 +88,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
Nameops.out_name x,None,compose_prod real_args (mkSort new_sort)
in
let new_predicates =
- list_map_i
+ List.map_i
change_predicate_sort
0
princ_type_info.predicates
@@ -252,7 +252,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
in
let pre_res =
replace_vars
- (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
+ (List.map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
(lift (List.length ptes_vars) pre_res)
in
it_mkProd_or_LetIn
@@ -460,7 +460,7 @@ let get_funs_constant mp dp =
let first_params = List.hd l_params in
List.iter
(fun params ->
- if not (list_equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params)
+ if not (List.equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params)
then error "Not a mutal recursive block"
)
l_params
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index d11c01672a..1c21934495 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -89,7 +89,7 @@ let combine_results
in (* and then we flatten the map *)
{
result = List.concat pre_result;
- to_avoid = list_union res1.to_avoid res2.to_avoid
+ to_avoid = List.union res1.to_avoid res2.to_avoid
}
@@ -269,7 +269,7 @@ let make_discr_match_el =
end
*)
let make_discr_match_brl i =
- list_map_i
+ List.map_i
(fun j (_,idl,patl,_) ->
if j=i
then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref))
@@ -659,7 +659,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let case_pats = build_constructors_of_type ind [] in
assert (Array.length case_pats = 2);
let brl =
- list_map_i
+ List.map_i
(fun i x -> (Loc.ghost,[],[case_pats.(i)],x))
0
[lhs;rhs]
@@ -748,7 +748,7 @@ and build_entry_lc_from_case env funname make_discr
{
result = List.concat (List.map (fun r -> r.result) results);
to_avoid =
- List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
+ List.fold_left (fun acc r -> List.union acc r.to_avoid) [] results
}
and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
@@ -818,7 +818,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
let those_pattern_preconds =
(List.flatten
(
- list_map3
+ List.map3
(fun pat e typ_as_constr ->
let this_pat_ids = ids_of_pat pat in
let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in
@@ -977,7 +977,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let mib,_ = Global.lookup_inductive ind in
let nparam = mib.Declarations.mind_nparams in
let params,arg' =
- ((Util.list_chop nparam args'))
+ ((Util.List.chop nparam args'))
in
let rt_typ =
GApp(Loc.ghost,
@@ -1000,7 +1000,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
match kind_of_term eq'_as_constr with
| App(_,[|_;_;ty;_|]) ->
let ty = Array.to_list (snd (destApp ty)) in
- let ty' = snd (Util.list_chop nparam ty) in
+ let ty' = snd (Util.List.chop nparam ty) in
List.fold_left2
(fun acc var_as_constr arg ->
if isRel var_as_constr
@@ -1238,7 +1238,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
let l = ref [] in
let _ =
try
- list_iter_i
+ List.iter_i
(fun i ((n,nt,is_defined) as param) ->
if array_for_all
(fun l ->
@@ -1362,7 +1362,7 @@ let do_build_inductive
in
let rel_arity i funargs = (* Reduilding arities (with parameters) *)
let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list =
- (snd (list_chop nrel_params funargs))
+ (snd (List.chop nrel_params funargs))
in
List.fold_right
(fun (n,t,is_defined) acc ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 52562fb374..18b2bbe2f7 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -21,7 +21,7 @@ let is_rec_info scheme_info =
Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
)
in
- Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
+ Util.List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
let choose_dest_or_ind scheme_info =
if is_rec_info scheme_info
@@ -337,7 +337,7 @@ let generate_principle on_error
in
let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
let _ =
- list_map_i
+ List.map_i
(fun i x ->
let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
let princ_type = Typeops.type_of_constant (Global.env()) princ
@@ -392,7 +392,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
if List.length names = 1 then 1
else error "Recursive argument must be specified"
| Some wf_arg ->
- list_index (Name wf_arg) names
+ List.index (Name wf_arg) names
in
let unbounded_eq =
let f_app_args =
@@ -516,7 +516,7 @@ let decompose_lambda_n_assum_constr_expr =
(n - nal_length)
(Constrexpr.CLambdaN(lambda_loc,bl,e'))
else
- let nal_keep,nal_expr = list_chop n nal in
+ let nal_keep,nal_expr = List.chop n nal in
(List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
)
@@ -548,7 +548,7 @@ let decompose_prod_n_assum_constr_expr =
(if bl = [] then e' else (Constrexpr.CLambdaN(lambda_loc,bl,e')))
else
(* let _ = Pp.msgnl (str "second case") in *)
- let nal_keep,nal_expr = list_chop n nal in
+ let nal_keep,nal_expr = List.chop n nal in
(List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
)
@@ -585,7 +585,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
let lnal' = List.length nal' in
if lnal' >= lnal
then
- let old_nal',new_nal' = list_chop lnal nal' in
+ let old_nal',new_nal' = List.chop lnal nal' in
rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(make_assoc assoc old_nal' nal)) bl'
(if new_nal' = [] && rest = []
then typ'
@@ -593,7 +593,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
then CProdN(Loc.ghost,rest,typ')
else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ'))
else
- let captured_nal,non_captured_nal = list_chop lnal' nal in
+ let captured_nal,non_captured_nal = List.chop lnal' nal in
rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (make_assoc assoc nal' captured_nal))
bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ'))
| _ -> assert false
@@ -789,7 +789,7 @@ let rec chop_n_arrow n t =
else
let new_t' =
Constrexpr.CProdN(Loc.ghost,
- ((snd (list_chop n nal)),k,t'')::nal_ta',t')
+ ((snd (List.chop n nal)),k,t'')::nal_ta',t')
in
raise (Stop new_t')
in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2f6a6a7d7b..1d1089a549 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -370,7 +370,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
in
(* in fact we must also add the parameters to the constructor args *)
let constructor_args g =
- let params_id = fst (list_chop princ_infos.nparams args_names) in
+ let params_id = fst (List.chop princ_infos.nparams args_names) in
(List.map mkVar params_id)@((constructor_args g))
in
(* We then get the constructor corresponding to this branch and
@@ -446,7 +446,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
)
lemmas_types_infos
in
- let param_names = fst (list_chop princ_infos.nparams args_names) in
+ let param_names = fst (List.chop princ_infos.nparams args_names) in
let params = List.map mkVar param_names in
let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in
(* The bindings of the principle
@@ -611,7 +611,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
in
(* in fact we must also add the parameters to the constructor args *)
let constructor_args =
- let params_id = fst (list_chop princ_infos.nparams args_names) in
+ let params_id = fst (List.chop princ_infos.nparams args_names) in
(List.map mkVar params_id)@(List.rev constructor_args)
in
(* We then get the constructor corresponding to this branch and
@@ -669,7 +669,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
g
in
(* end of branche proof *)
- let param_names = fst (list_chop princ_infos.nparams args_names) in
+ let param_names = fst (List.chop princ_infos.nparams args_names) in
let params = List.map mkVar param_names in
let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in
(* The bindings of the principle
@@ -996,7 +996,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
]
g
in
- let params_names = fst (list_chop princ_infos.nparams args_names) in
+ let params_names = fst (List.chop princ_infos.nparams args_names) in
let params = List.map mkVar params_names in
tclTHENSEQ
[ tclMAP h_intro (args_names@[res;hres]);
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 4fe22a3543..21c0d86a4f 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -165,11 +165,11 @@ let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a =
let res = f !i acc x in i := !i + 1; res)
acc arr
-(* Like list_chop but except that [i] is the size of the suffix of [l]. *)
+(* Like List.chop but except that [i] is the size of the suffix of [l]. *)
let list_chop_end i l =
let size_prefix = List.length l -i in
if size_prefix < 0 then failwith "list_chop_end"
- else list_chop size_prefix l
+ else List.chop size_prefix l
let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a =
let i = ref 0 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 14d9b7fcb0..8b0fc27397 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -705,7 +705,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
(try
(tclTHENS
destruct_tac
- (list_map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
+ (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
))
with
| UserError("Refiner.thensn_tac3",_)
@@ -1014,7 +1014,7 @@ let compute_terminate_type nb_args func =
Array.of_list
(lift 5 a_arrow_b:: mkRel 3::
constr_of_global func::mkRel 1::
- List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
+ List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
)
)
in
@@ -1044,7 +1044,7 @@ let termination_proof_header is_mes input_type ids args_id relation
let nargs = List.length args_id in
let pre_rec_args =
List.rev_map
- mkVar (fst (list_chop (rec_arg_num - 1) args_id))
+ mkVar (fst (List.chop (rec_arg_num - 1) args_id))
in
let relation = substl pre_rec_args relation in
let input_type = substl pre_rec_args input_type in
@@ -1297,7 +1297,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
(Elim.h_decompose_and (mkVar hid))
(fun g ->
let ids' = pf_ids_of_hyps g in
- lid := List.rev (list_subtract ids' ids);
+ lid := List.rev (List.subtract ids' ids);
if !lid = [] then lid := [hid];
tclIDTAC g
)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 10:55:45 +0000