aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml36
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml410
-rw-r--r--tactics/eauto.ml48
-rw-r--r--tactics/elim.ml4
-rw-r--r--tactics/eqdecide.ml42
-rw-r--r--tactics/eqschemes.ml18
-rw-r--r--tactics/equality.ml12
-rw-r--r--tactics/hipattern.ml42
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/refine.ml4
-rw-r--r--tactics/rewrite.ml42
-rw-r--r--tactics/tacinterp.ml24
-rw-r--r--tactics/tacticals.ml10
-rw-r--r--tactics/tactics.ml28
-rw-r--r--tactics/tauto.ml42
17 files changed, 85 insertions, 85 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 5068552d17..be1e8e7017 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -280,7 +280,7 @@ let subst_path_atom subst p =
| PathAny -> p
| PathHints grs ->
let gr' gr = fst (subst_global subst gr) in
- let grs' = list_smartmap gr' grs in
+ let grs' = List.smartmap gr' grs in
if grs' == grs then p else PathHints grs'
let rec subst_hints_path subst hp =
@@ -393,7 +393,7 @@ module Hint_db = struct
let add_list l db = List.fold_left (fun db k -> add_one k db) db l
- let remove_sdl p sdl = list_smartfilter p sdl
+ let remove_sdl p sdl = List.smartfilter p sdl
let remove_he st p (sl1, sl2, dn as he) =
let sl1' = remove_sdl p sl1 and sl2' = remove_sdl p sl2 in
if sl1' == sl1 && sl2' == sl2 then he
@@ -402,7 +402,7 @@ module Hint_db = struct
let remove_list grs db =
let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in
let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
- let hintnopat = list_smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
+ let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
{ db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
let remove_one gr db = remove_list [gr] db
@@ -691,14 +691,14 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
match hintlist with
| CreateDB _ -> obj
| AddTransparency (grs, b) ->
- let grs' = list_smartmap (subst_evaluable_reference subst) grs in
+ let grs' = List.smartmap (subst_evaluable_reference subst) grs in
if grs==grs' then obj else (local, name, AddTransparency (grs', b))
| AddHints hintlist ->
- let hintlist' = list_smartmap subst_hint hintlist in
+ let hintlist' = List.smartmap subst_hint hintlist in
if hintlist' == hintlist then obj else
(local,name,AddHints hintlist')
| RemoveHints grs ->
- let grs' = list_smartmap (fun x -> fst (subst_global subst x)) grs in
+ let grs' = List.smartmap (fun x -> fst (subst_global subst x)) grs in
if grs==grs' then obj else (local, name, RemoveHints grs')
| AddCut path ->
let path' = subst_hints_path subst path in
@@ -761,7 +761,7 @@ let add_extern pri pat tacast local dbname =
let tacmetas = [] in
match pat with
| Some (patmetas,pat) ->
- (match (list_subtract tacmetas patmetas) with
+ (match (List.subtract tacmetas patmetas) with
| i::_ ->
errorlabstrm "add_extern"
(str "The meta-variable ?" ++ Ppconstr.pr_patvar i ++ str" is not bound.")
@@ -859,7 +859,7 @@ let interp_hints h =
let constr_hints_of_ind qid =
let ind = global_inductive_with_alias qid in
Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
- list_tabulate (fun i -> let c = (ind,i+1) in
+ List.tabulate (fun i -> let c = (ind,i+1) in
None, true, PathHints [ConstructRef c], mkConstruct c)
(nconstructors ind) in
HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
@@ -1054,10 +1054,10 @@ let unify_resolve_gen = function
(* Util *)
let expand_constructor_hints env lems =
- list_map_append (fun (sigma,lem) ->
+ List.map_append (fun (sigma,lem) ->
match kind_of_term lem with
| Ind ind ->
- list_tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind)
+ List.tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind)
| _ ->
[prepare_hint env (sigma,lem)]) lems
@@ -1067,7 +1067,7 @@ let expand_constructor_hints env lems =
let add_hint_lemmas eapply lems hint_db gl =
let lems = expand_constructor_hints (pf_env gl) lems in
let hintlist' =
- list_map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in
+ List.map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in
Hint_db.add_list hintlist' hint_db
let make_local_hint_db ?ts eapply lems gl =
@@ -1076,7 +1076,7 @@ let make_local_hint_db ?ts eapply lems gl =
| None -> Hint_db.transparent_state (searchtable_map "core")
| Some ts -> ts
in
- let hintlist = list_map_append (pf_apply make_resolve_hyp gl) sign in
+ let hintlist = List.map_append (pf_apply make_resolve_hyp gl) sign in
add_hint_lemmas eapply lems
(Hint_db.add_list hintlist (Hint_db.empty ts false)) gl
@@ -1271,7 +1271,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db gl =
and my_find_search_nodelta db_list local_db hdc concl =
List.map (fun hint -> (None,hint))
- (list_map_append (hintmap_of hdc concl) (local_db::db_list))
+ (List.map_append (hintmap_of hdc concl) (local_db::db_list))
and my_find_search mod_delta =
if mod_delta then my_find_search_delta
@@ -1281,7 +1281,7 @@ and my_find_search_delta db_list local_db hdc concl =
let flags = {auto_unif_flags with use_metas_eagerly_in_conv_on_closed_terms = true} in
let f = hintmap_of hdc concl in
if occur_existential concl then
- list_map_append
+ List.map_append
(fun db ->
if Hint_db.use_dn db then
let flags = flags_of_state (Hint_db.transparent_state db) in
@@ -1291,7 +1291,7 @@ and my_find_search_delta db_list local_db hdc concl =
List.map (fun x -> (Some flags,x)) (f db))
(local_db::db_list)
else
- list_map_append (fun db ->
+ List.map_append (fun db ->
if Hint_db.use_dn db then
let flags = flags_of_state (Hint_db.transparent_state db) in
List.map (fun x -> (Some flags, x)) (f db)
@@ -1346,7 +1346,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
let make_db_list dbnames =
let use_core = not (List.mem "nocore" dbnames) in
- let dbnames = list_remove "nocore" dbnames in
+ let dbnames = List.remove "nocore" dbnames in
let dbnames = if use_core then "core"::dbnames else dbnames in
let lookup db =
try searchtable_map db with Not_found -> error_no_such_hint_database db
@@ -1361,7 +1361,7 @@ let trivial ?(debug=Off) lems dbnames gl =
let full_trivial ?(debug=Off) lems gl =
let dbnames = Hintdbmap.dom !searchtable in
- let dbnames = list_remove "v62" dbnames in
+ let dbnames = List.remove "v62" dbnames in
let db_list = List.map (fun x -> searchtable_map x) dbnames in
let d = mk_trivial_dbg debug in
tclTRY_dbg d
@@ -1454,7 +1454,7 @@ let default_auto = auto !default_search_depth [] []
let delta_full_auto ?(debug=Off) mod_delta n lems gl =
let dbnames = Hintdbmap.dom !searchtable in
- let dbnames = list_remove "v62" dbnames in
+ let dbnames = List.remove "v62" dbnames in
let db_list = List.map (fun x -> searchtable_map x) dbnames in
let d = mk_auto_dbg debug in
tclTRY_dbg d
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index d2d18c53b3..dfa94102d0 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -207,7 +207,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl =
(* Functions necessary to the library object declaration *)
let cache_hintrewrite (_,(rbase,lrl)) =
let base = try find_base rbase with _ -> HintDN.empty in
- let max = try fst (Util.list_last (HintDN.find_all base)) with _ -> 0 in
+ let max = try fst (Util.List.last (HintDN.find_all base)) with _ -> 0 in
let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 78df21a6d5..1eecb1eb30 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -159,7 +159,7 @@ and e_my_find_search db_list local_db hdc complete concl =
let prods, concl = decompose_prod_assum concl in
let nprods = List.length prods in
let hintl =
- list_map_append
+ List.map_append
(fun db ->
if Hint_db.use_dn db then
let flags = flags_of_state (Hint_db.transparent_state db) in
@@ -251,7 +251,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
let hints =
if is_class then
let hints = build_subclasses ~check:false env sigma (VarRef id) None in
- (list_map_append
+ (List.map_append
(fun (pri, c) -> make_resolves env sigma
(true,false,Flags.is_verbose()) pri c)
hints)
@@ -376,7 +376,7 @@ let hints_tac hints =
(* Reorder with dependent subgoals. *)
(gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s')
in
- let gls' = list_map_i
+ let gls' = List.map_i
(fun j (evar, g) ->
let info =
{ info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
@@ -472,7 +472,7 @@ let cut_of_hints h =
let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs evm' =
let cut = cut_of_hints hints in
- { it = list_map_i (fun i g ->
+ { it = List.map_i (fun i g ->
let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'} in
(gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
@@ -779,7 +779,7 @@ END
let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
try
- let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
+ let dbs = List.map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 28840669f9..fd5fbe25ac 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -119,11 +119,11 @@ and e_my_find_search db_list local_db hdc concl =
let hdc = head_of_constr_reference hdc in
let hintl =
if occur_existential concl then
- list_map_append (fun db ->
+ List.map_append (fun db ->
let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
else
- list_map_append (fun db ->
+ List.map_append (fun db ->
let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
in
@@ -261,7 +261,7 @@ module SearchProblem = struct
{ depth = pred s.depth; tacres = res;
dblist = s.dblist; last_tactic = pp; prev = ps;
localdb =
- list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
+ List.addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
l
in
List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
@@ -364,7 +364,7 @@ let eauto ?(debug=Off) np lems dbnames =
let full_eauto ?(debug=Off) n lems gl =
let dbnames = current_db_names () in
- let dbnames = list_remove "v62" dbnames in
+ let dbnames = List.remove "v62" dbnames in
let db_list = List.map searchtable_map dbnames in
tclTRY (e_search_auto debug n lems db_list) gl
diff --git a/tactics/elim.ml b/tactics/elim.ml
index a2ec6dfa56..32acc5af57 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -37,10 +37,10 @@ let introCaseAssumsThen tac ba =
let n1 = List.length case_thin_sign in
let n2 = List.length ba.branchnames in
let (l1,l2),l3 =
- if n1 < n2 then list_chop n1 ba.branchnames, []
+ if n1 < n2 then List.chop n1 ba.branchnames, []
else
(ba.branchnames, []),
- if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in
+ if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in
let introCaseAssums =
tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in
(tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 7bc372ca93..f26eb10241 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -129,7 +129,7 @@ let solveEqBranch rectype g =
let (eqonleft,op,lhs,rhs,_) = match_eqdec (pf_concl g) in
let (mib,mip) = Global.lookup_inductive rectype in
let nparams = mib.mind_nparams in
- let getargs l = list_skipn nparams (snd (decompose_app l)) in
+ let getargs l = List.skipn nparams (snd (decompose_app l)) in
let rargs = getargs rhs
and largs = getargs lhs in
List.fold_right2
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f744b015ad..33eb7c6185 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -63,7 +63,7 @@ let default_id_of_sort = function InProp | InSet -> hid | InType -> xid
let fresh env id = next_global_ident_away id []
let build_dependent_inductive ind (mib,mip) =
- let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+ let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
applist
(mkInd ind,
extended_rel_list mip.mind_nrealargs_ctxt mib.mind_params_ctxt
@@ -96,20 +96,20 @@ let get_sym_eq_data env ind =
let (mib,mip as specif) = lookup_mind_specif env ind in
if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
error "Not an inductive type with a single constructor.";
- let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+ let realsign,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
if List.exists (fun (_,b,_) -> b <> None) realsign then
error "Inductive equalities with local definitions in arity not supported.";
let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
error "Constructor must have no arguments"; (* This can be relaxed... *)
- let params,constrargs = list_chop mib.mind_nparams constrargs in
+ let params,constrargs = List.chop mib.mind_nparams constrargs in
if mip.mind_nrealargs > mib.mind_nparams then
error "Constructors arguments must repeat the parameters.";
- let _,params2 = list_chop (mib.mind_nparams-mip.mind_nrealargs) params in
+ let _,params2 = List.chop (mib.mind_nparams-mip.mind_nrealargs) params in
let paramsctxt1,_ =
- list_chop (mib.mind_nparams-mip.mind_nrealargs) mib.mind_params_ctxt in
- if not (list_equal eq_constr params2 constrargs) then
+ List.chop (mib.mind_nparams-mip.mind_nrealargs) mib.mind_params_ctxt in
+ if not (List.equal eq_constr params2 constrargs) then
error "Constructors arguments must repeat the parameters.";
(* nrealargs_ctxt and nrealargs are the same here *)
(specif,mip.mind_nrealargs,realsign,mib.mind_params_ctxt,paramsctxt1)
@@ -128,14 +128,14 @@ let get_non_sym_eq_data env ind =
let (mib,mip as specif) = lookup_mind_specif env ind in
if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
error "Not an inductive type with a single constructor.";
- let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+ let realsign,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
if List.exists (fun (_,b,_) -> b <> None) realsign then
error "Inductive equalities with local definitions in arity not supported";
let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
error "Constructor must have no arguments";
- let _,constrargs = list_chop mib.mind_nparams constrargs in
+ let _,constrargs = List.chop mib.mind_nparams constrargs in
(specif,constrargs,realsign,mip.mind_nrealargs)
(**********************************************************************)
@@ -679,7 +679,7 @@ let build_congr env (eq,refl) ind =
if mip.mind_nrealargs <> 1 then
error "Expect an inductive type with one predicate parameter.";
let i = 1 in
- let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+ let realsign,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
if List.exists (fun (_,b,_) -> b <> None) realsign then
error "Inductive equalities with local definitions in arity not supported.";
let env_with_arity = push_rel_context mip.mind_arity_ctxt env in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b4cb48285f..4d67fef006 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -397,7 +397,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
(* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
let ids =
let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
- Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl)
+ Idset.fold (fun id l -> List.remove id l) ids_in_c (pf_ids_of_hyps gl)
in do_hyps_atleastonce ids gl
in
if cl.concl_occs = NoOccurrences then do_hyps else
@@ -532,15 +532,15 @@ let find_positions env sigma t1 t2 =
| Construct sp1, Construct sp2
when List.length args1 = mis_constructor_nargs_env env sp1
->
- let sorts = list_intersect sorts (allowed_sorts env (fst sp1)) in
+ let sorts = List.intersect sorts (allowed_sorts env (fst sp1)) in
(* both sides are fully applied constructors, so either we descend,
or we can discriminate here. *)
if is_conv env sigma hd1 hd2 then
let nrealargs = constructor_nrealargs env sp1 in
- let rargs1 = list_lastn nrealargs args1 in
- let rargs2 = list_lastn nrealargs args2 in
+ let rargs1 = List.lastn nrealargs args1 in
+ let rargs2 = List.lastn nrealargs args2 in
List.flatten
- (list_map2_i (fun i -> findrec sorts ((sp1,i)::posn))
+ (List.map2_i (fun i -> findrec sorts ((sp1,i)::posn))
0 rargs1 rargs2)
else if List.mem InType sorts then (* see build_discriminator *)
raise (DiscrFound (List.rev posn,sp1,sp2))
@@ -1495,7 +1495,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) gl =
with PatternMatchingFailure -> failwith "caught"
in
let ids = map_succeed test (pf_hyps_types gl) in
- let ids = list_uniquize ids in
+ let ids = List.uniquize ids in
subst_gen flags.rewrite_dependent_proof ids gl
(* Rewrite the first assumption for which the condition faildir does not fail
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index a6dcb9d585..bb35cedeae 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -319,7 +319,7 @@ let match_with_nodep_ind t =
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
+ fst (List.chop mib.mind_nparams args) in
Some (hdapp,params,mip.mind_nrealargs)
else
None
diff --git a/tactics/inv.ml b/tactics/inv.ml
index cb1ffb3856..189c73a167 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -111,7 +111,7 @@ let make_inv_predicate env sigma indf realargs id status concl =
let nhyps = rel_context_length hyps in
let env' = push_rel_context hyps env in
let realargs' = List.map (lift nhyps) realargs in
- let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in
+ let pairs = List.map_i (compute_eqn env' sigma nhyps) 0 realargs' in
(* Now the arity is pushed, and we need to construct the pairs
* ai,mkRel(n-i+1) *)
(* Now, we can recurse down this list, for each ai,(mkRel k) whether to
@@ -469,7 +469,7 @@ let raw_inversion inv_kind id status names gl =
(fun id ->
(tclTHEN
(apply_term (mkVar id)
- (list_tabulate (fun _ -> Evarutil.mk_new_meta()) neqns))
+ (List.tabulate (fun _ -> Evarutil.mk_new_meta()) neqns))
reflexivity))])
gl
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 5242d0f3e9..3031734fb7 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -187,7 +187,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
compute_first_inversion_scheme env sigma ind sort dep_option
in
assert
- (list_subset
+ (List.subset
(global_vars env invGoal)
(ids_of_named_context (named_context invEnv)));
(*
diff --git a/tactics/refine.ml b/tactics/refine.ml
index fc2da8d0a9..1cb4f01e22 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -348,7 +348,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
| _ -> 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 firsts,lasts = list_chop j (Array.to_list fixes) in
+ let firsts,lasts = List.chop j (Array.to_list fixes) in
tclTHENS
(tclTHEN
(ensure_products (succ ni.(j)))
@@ -365,7 +365,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
| _ -> error "Recursive functions must have names."
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
+ let firsts,lasts = List.chop j (Array.to_list cofixes) in
tclTHENS
(mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j)
(List.map (function
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index f9aa1f0257..c36ab2f83a 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -725,7 +725,7 @@ let fold_match ?(force=false) env sigma c =
in
let app =
let ind, args = Inductive.find_rectype env cty in
- let pars, args = list_chop ci.ci_npar args in
+ let pars, args = List.chop ci.ci_npar args in
let meths = List.map (fun br -> br) (Array.to_list brs) in
applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b0997c067d..4ce382df24 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -92,7 +92,7 @@ let catch_error call_trace tac g =
| LtacLocated _ as e -> raise e
| Loc.Exc_located (_,LtacLocated _) as e -> raise e
| e ->
- let (nrep,loc',c),tail = list_sep_last call_trace in
+ let (nrep,loc',c),tail = List.sep_last call_trace in
let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
if tail = [] then
let loc = if loc = dloc then loc' else loc in
@@ -928,7 +928,7 @@ and intern_match_rule onlytac ist = function
let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
let ido,metas2,pat = intern_pattern ist lfun mp in
- let metas = list_uniquize (metas1@metas2) in
+ let metas = List.uniquize (metas1@metas2) in
let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
| [] -> []
@@ -1329,7 +1329,7 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
(*all of dest_fun, List.assoc, constr_list_of_VList may raise Not_found*)
let sigma, c = interp_fun ist env sigma x in
sigma, [c] in
- let sigma, l = list_fold_map try_expand_ltac_var sigma l in
+ let sigma, l = List.fold_map try_expand_ltac_var sigma l in
sigma, List.flatten l
let interp_constr_list ist env sigma c =
@@ -1541,7 +1541,7 @@ let interp_bindings ist env sigma = function
let sigma, l = interp_open_constr_list ist env sigma l in
sigma, ImplicitBindings l
| ExplicitBindings l ->
- let sigma, l = list_fold_map (interp_binding ist env) sigma l in
+ let sigma, l = List.fold_map (interp_binding ist env) sigma l in
sigma, ExplicitBindings l
let interp_constr_with_bindings ist env sigma (c,bl) =
@@ -1556,8 +1556,8 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) =
let loc_of_bindings = function
| NoBindings -> Loc.ghost
-| ImplicitBindings l -> loc_of_glob_constr (fst (list_last l))
-| ExplicitBindings l -> pi1 (list_last l)
+| ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
+| ExplicitBindings l -> pi1 (List.last l)
let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) =
let loc1 = loc_of_glob_constr c in
@@ -1982,7 +1982,7 @@ and eval_with_fail ist is_lazy goal tac =
(* Interprets the clauses of a recursive LetIn *)
and interp_letrec ist gl llc u =
let lref = ref ist.lfun in
- let lve = list_map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg (dloc,b)))) llc in
+ let lve = List.map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg (dloc,b)))) llc in
lref := lve@ist.lfun;
let ist = { ist with lfun = lve@ist.lfun } in
val_interp ist gl u
@@ -2069,7 +2069,7 @@ and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
try
let id_match = pi1 hyp_match in
- let nextlhyps = list_remove_assoc_in_triple id_match lhyps_rest in
+ let nextlhyps = List.remove_assoc_in_triple id_match lhyps_rest in
apply_hyps_context_rec (lfun@lids) lm nextlhyps tl
with e when is_match_catchable e ->
match_next_pattern find_next' in
@@ -2335,7 +2335,7 @@ and interp_atomic ist gl tac =
(h_vm_cast_no_check c_interp)
| TacApply (a,ev,cb,cl) ->
let sigma, l =
- list_fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
+ List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
in
let tac = match cl with
| None -> h_apply a ev
@@ -2435,7 +2435,7 @@ and interp_atomic ist gl tac =
h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
| TacInductionDestruct (isrec,ev,(l,el,cls)) ->
let sigma, l =
- list_fold_map (fun sigma (c,(ipato,ipats)) ->
+ List.fold_map (fun sigma (c,(ipato,ipats)) ->
let c = interp_induction_arg ist gl c in
(sigma,(c,
(Option.map (interp_intro_pattern ist gl) ipato,
@@ -2492,7 +2492,7 @@ and interp_atomic ist gl tac =
let sigma, bl = interp_bindings ist env sigma bl in
tclWITHHOLES ev (h_right ev) sigma bl
| TacSplit (ev,_,bll) ->
- let sigma, bll = list_fold_map (interp_bindings ist env) sigma bll in
+ let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
tclWITHHOLES ev (h_split ev) sigma bll
| TacAnyConstructor (ev,t) ->
abstract_tactic (TacAnyConstructor (ev,t))
@@ -3142,7 +3142,7 @@ let add_tacdef local isrec tacl =
let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
let ist =
{(make_empty_glob_sign()) with ltacrecvars =
- if isrec then list_map_filter
+ if isrec then List.map_filter
(function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun
else []} in
let gtacl =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index aaa75a4e26..f88530eec3 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -87,7 +87,7 @@ let lastHypId gl = nthHypId 1 gl
let lastHyp gl = nthHyp 1 gl
let nLastDecls n gl =
- try list_firstn n (pf_hyps gl)
+ try List.firstn n (pf_hyps gl)
with Failure _ -> error "Not enough hypotheses in the goal."
let nLastHypsId n gl = List.map pi1 (nLastDecls n gl)
@@ -108,7 +108,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac
let onNLastHyps n tac = onHyps (nLastHyps n) tac
let afterHyp id gl =
- fst (list_split_when (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
+ fst (List.split_when (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
(***************************************)
(* Clause Tacticals *)
@@ -174,7 +174,7 @@ let fix_empty_or_and_pattern nv l =
names and "[ ]" for no clause at all *)
(* 2- More generally, we admit "[ ]" for any disjunctive pattern of
arbitrary length *)
- if l = [[]] then list_make nv [] else l
+ if l = [[]] then List.make nv [] else l
let check_or_and_pattern_size loc names n =
if List.length names <> n then
@@ -335,7 +335,7 @@ let make_elim_branch_assumptions ba gl =
| (_, _) -> anomaly "make_elim_branch_assumptions"
in
makerec ([],[],[],[],[]) ba.branchsign
- (try list_firstn ba.nassums (pf_hyps gl)
+ (try List.firstn ba.nassums (pf_hyps gl)
with Failure _ -> anomaly "make_elim_branch_assumptions")
let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
@@ -359,7 +359,7 @@ let make_case_branch_assumptions ba gl =
| (_, _) -> anomaly "make_case_branch_assumptions"
in
makerec ([],[],[],[]) ba.branchsign
- (try list_firstn ba.nassums (pf_hyps gl)
+ (try List.firstn ba.nassums (pf_hyps gl)
with Failure _ -> anomaly "make_case_branch_assumptions")
let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1ccb3ffdb2..b1a9c6732f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -857,7 +857,7 @@ let clenv_fchain_in id ?(flags=elim_flags) mv elimclause hypclause =
let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause indclause gl =
let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
let hypmv =
- try match list_remove indmv (clenv_independent elimclause) with
+ try match List.remove indmv (clenv_independent elimclause) with
| [a] -> a
| _ -> failwith ""
with Failure _ -> errorlabstrm "elimination_clause"
@@ -929,7 +929,7 @@ let descend_in_conjunctions tac exit c gl =
let elim = pf_apply build_case_analysis_scheme gl ind false sort in
NotADefinedRecordUseScheme elim in
tclFIRST
- (list_tabulate (fun i gl ->
+ (List.tabulate (fun i gl ->
match make_projection (project gl) params cstr sign elim i n c with
| None -> tclFAIL 0 (mt()) gl
| Some (p,pt) ->
@@ -1025,7 +1025,7 @@ let progress_with_clause flags innerclause clause =
if ordered_metas = [] then error "Statement without assumptions.";
let f mv =
find_matching_clause (clenv_fchain mv ~flags clause) innerclause in
- try list_try_find f ordered_metas
+ try List.try_find f ordered_metas
with Failure _ -> error "Unable to unify."
let apply_in_once_main flags innerclause (d,lbind) gl =
@@ -1164,7 +1164,7 @@ let specialize mopt (c,lbind) g =
let nargs = List.length tstack in
let tstack = match mopt with
| Some m ->
- if m < nargs then list_firstn m tstack else tstack
+ if m < nargs then List.firstn m tstack else tstack
| None ->
let rec chk = function
| [] -> []
@@ -1565,8 +1565,8 @@ let generalize_dep ?(with_let=false) c gl =
let generalize_gen_let lconstr gl =
let newcl =
- list_fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in
- apply_type newcl (list_map_filter (fun ((_,c,b),_) ->
+ List.fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in
+ apply_type newcl (List.map_filter (fun ((_,c,b),_) ->
if b = None then Some c else None) lconstr) gl
let generalize_gen lconstr =
@@ -1753,7 +1753,7 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
| Some occ ->
subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None (pf_concl gl)) in
let lastlhyp =
- if depdecls = [] then MoveLast else MoveAfter(pi1(list_last depdecls)) in
+ if depdecls = [] then MoveLast else MoveAfter(pi1(List.last depdecls)) in
(depdecls,lastlhyp,ccl,out test)
let letin_tac_gen with_eq name (sigmac,c) test ty occs gl =
@@ -1998,7 +1998,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 gl =
let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
let prods, indtyp = decompose_prod typ0 in
let argl = snd (decompose_app indtyp) in
- let params = list_firstn nparams argl in
+ let params = List.firstn nparams argl in
(* le gl est important pour ne pas préévaluer *)
let rec atomize_one i avoid gl =
if i<>nparams then
@@ -2031,7 +2031,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 gl =
let find_atomic_param_of_ind nparams indtyp =
let argl = snd (decompose_app indtyp) in
let argv = Array.of_list argl in
- let params = list_firstn nparams argl in
+ let params = List.firstn nparams argl in
let indvars = ref Idset.empty in
for i = nparams to (Array.length argv)-1 do
match kind_of_term argv.(i) with
@@ -2749,8 +2749,8 @@ let compute_scheme_signature scheme names_info ind_type_guess =
(* Check again conclusion *)
let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f = IndArg in
let ind_is_ok =
- list_equal eq_constr
- (list_lastn scheme.nargs indargs)
+ List.equal eq_constr
+ (List.lastn scheme.nargs indargs)
(extended_rel_list 0 scheme.args) in
if not (ccl_arg_ok & ind_is_ok) then
error_ind_scheme "the conclusion of"
@@ -2895,11 +2895,11 @@ let recolle_clenv nparams lid elimclause gl =
let nidargs = List.length lidargs in
(* parameters correspond to first elts of lid. *)
let clauses_params =
- list_map_i (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(i))
+ List.map_i (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(i))
0 lidparams in
(* arguments correspond to last elts of lid. *)
let clauses_args =
- list_map_i
+ List.map_i
(fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(nmv-nidargs+i))
0 lidargs in
let clauses = clauses_params@clauses_args in
@@ -3087,7 +3087,7 @@ let clear_unselected_context id inhyps cls gl =
(* erase if not selected and dependent on id or selected hyps *)
let test id = occur_var_in_decl (pf_env gl) id d in
if List.exists test (id::inhyps) then Some id' else None in
- let ids = list_map_filter to_erase (pf_hyps gl) in
+ let ids = List.map_filter to_erase (pf_hyps gl) in
thin ids gl
| None -> tclIDTAC gl
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 9696696684..fdfc2b7834 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -173,7 +173,7 @@ let flatten_contravariant_disj flags ist =
typ with
| Some (_,args) ->
let hyp = valueIn (VConstr ([],hyp)) in
- iter_tac (list_map_i (fun i arg ->
+ iter_tac (List.map_i (fun i arg ->
let typ = valueIn (VConstr ([],mkArrow arg c)) in
let i = Tacexpr.Integer i in
<:tactic<
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 17:58:48 +0000