aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/functional_principles_proofs.ml12
-rw-r--r--plugins/funind/functional_principles_types.ml16
-rw-r--r--plugins/funind/invfun.ml8
-rw-r--r--pretyping/namegen.ml4
-rw-r--r--pretyping/termops.ml16
-rw-r--r--pretyping/termops.mli16
-rw-r--r--tactics/eqschemes.ml4
-rw-r--r--tactics/tactics.ml4
8 files changed, 39 insertions, 41 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 4f96ce06e0..bc12fcea9c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -388,7 +388,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
let coq_I = Coqlib.build_coq_I () in
let rec scan_type context type_of_hyp : tactic =
if isLetIn type_of_hyp then
- let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in
+ let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
(* length of context didn't change ? *)
let new_context,new_typ_of_hyp =
@@ -406,13 +406,13 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
then
begin
let (x,t_x,t') = destProd type_of_hyp in
- let actual_real_type_of_hyp = it_mkProd_or_LetIn ~init:t' context in
+ let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in
if is_property ptes_infos t_x actual_real_type_of_hyp then
begin
let pte,pte_args = (destApp t_x) in
let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in
let popped_t' = pop t' in
- let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in
+ let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in
let prove_new_type_of_hyp =
let context_length = List.length context in
tclTHENLIST
@@ -463,7 +463,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
(* ); *)
let popped_t' = pop t' in
let real_type_of_hyp =
- it_mkProd_or_LetIn ~init:popped_t' context
+ it_mkProd_or_LetIn popped_t' context
in
let prove_trivial =
let nb_intro = List.length context in
@@ -491,7 +491,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
then (* t_x := t = t => we remove this precond *)
let popped_t' = pop t' in
let real_type_of_hyp =
- it_mkProd_or_LetIn ~init:popped_t' context
+ it_mkProd_or_LetIn popped_t' context
in
let hd,args = destApp t_x in
let get_args hd args =
@@ -954,7 +954,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args)
(Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
- let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in
+ let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
let f_id = id_of_label (con_label (destConst f)) in
let prove_replacement =
tclTHENSEQ
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 5ac5f9ce84..e0b08599d0 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -114,9 +114,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
in
let pre_princ =
it_mkProd_or_LetIn
- ~init:
(it_mkProd_or_LetIn
- ~init:(Option.fold_right
+ (Option.fold_right
mkProd_or_LetIn
princ_type_info.indarg
princ_type_info.concl
@@ -267,10 +266,10 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
(lift (List.length ptes_vars) pre_res)
in
it_mkProd_or_LetIn
- ~init:(it_mkProd_or_LetIn
- ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b)
- new_predicates)
- )
+ (it_mkProd_or_LetIn
+ pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b)
+ new_predicates)
+ )
princ_type_info.params
@@ -291,8 +290,7 @@ let change_property_sort toSort princ princName =
(fun i -> mkRel (nargs - i )))
in
it_mkLambda_or_LetIn
- ~init:
- (it_mkLambda_or_LetIn ~init
+ (it_mkLambda_or_LetIn init
(List.map change_sort_in_predicate princ_info.predicates)
)
princ_info.params
@@ -639,7 +637,7 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
const
with Found_type i ->
let princ_body =
- Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt
+ Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
in
{const with
Entries.const_entry_body = princ_body;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 90d7baeef4..f0ea133c60 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -248,7 +248,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
| [] | [_] | [_;_] -> anomaly "bad context"
| hres::res::(x,_,t)::ctxt ->
Termops.it_mkLambda_or_LetIn
- ~init:(Termops.it_mkProd_or_LetIn ~init:concl [hres;res])
+ (Termops.it_mkProd_or_LetIn concl [hres;res])
((x,None,t)::ctxt)
)
lemmas_types_infos
@@ -627,7 +627,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
*)
let lemmas =
Array.map
- (fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn ~init:concl ctxt))
+ (fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn concl ctxt))
lemmas_types_infos
in
(* We get the constant and the principle corresponding to this lemma *)
@@ -754,7 +754,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
generate_type false const_of_f graph i
in
- let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in
+ let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
let type_of_lemma = nf_zeta type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
type_of_lemma,type_info
@@ -809,7 +809,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
generate_type true const_of_f graph i
in
- let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in
+ let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
let type_of_lemma = nf_zeta type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
type_of_lemma,type_info
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index e7c9331527..c3c6b205d9 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -131,9 +131,9 @@ let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
let it_mkProd_or_LetIn_name env b hyps =
- it_mkProd_or_LetIn ~init:b (name_context env hyps)
+ it_mkProd_or_LetIn b (name_context env hyps)
let it_mkLambda_or_LetIn_name env b hyps =
- it_mkLambda_or_LetIn ~init:b (name_context env hyps)
+ it_mkLambda_or_LetIn b (name_context env hyps)
(**********************************************************************)
(* Fresh names *)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 17e0522230..d31242aa2b 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -235,18 +235,18 @@ let mkProd_wo_LetIn (na,body,t) c =
| None -> mkProd (na, t, c)
| Some b -> subst1 b c
-let it_mkProd ~init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init
-let it_mkLambda ~init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init
+let it_mkProd init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init
+let it_mkLambda init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init
let it_named_context_quantifier f ~init =
List.fold_left (fun c d -> f d c) init
-let it_mkProd_or_LetIn = it_named_context_quantifier mkProd_or_LetIn
-let it_mkProd_wo_LetIn = it_named_context_quantifier mkProd_wo_LetIn
-let it_mkLambda_or_LetIn = it_named_context_quantifier mkLambda_or_LetIn
-let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn
-let it_mkNamedProd_wo_LetIn = it_named_context_quantifier mkNamedProd_wo_LetIn
-let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
+let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init
+let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init
+let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init
+let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init
+let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init
+let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
(* *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 1346a7f524..385bd3022a 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -49,14 +49,14 @@ val extended_rel_vect : int -> rel_context -> constr array
(** iterators/destructors on terms *)
val mkProd_or_LetIn : rel_declaration -> types -> types
val mkProd_wo_LetIn : rel_declaration -> types -> types
-val it_mkProd : init:types -> (name * types) list -> types
-val it_mkLambda : init:constr -> (name * types) list -> constr
-val it_mkProd_or_LetIn : init:types -> rel_context -> types
-val it_mkProd_wo_LetIn : init:types -> rel_context -> types
-val it_mkLambda_or_LetIn : init:constr -> rel_context -> constr
-val it_mkNamedProd_or_LetIn : init:types -> named_context -> types
-val it_mkNamedProd_wo_LetIn : init:types -> named_context -> types
-val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr
+val it_mkProd : types -> (name * types) list -> types
+val it_mkLambda : constr -> (name * types) list -> constr
+val it_mkProd_or_LetIn : types -> rel_context -> types
+val it_mkProd_wo_LetIn : types -> rel_context -> types
+val it_mkLambda_or_LetIn : constr -> rel_context -> constr
+val it_mkNamedProd_or_LetIn : types -> named_context -> types
+val it_mkNamedProd_wo_LetIn : types -> named_context -> types
+val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
val it_named_context_quantifier :
(named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index a82eb86451..728f3fd72e 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -68,8 +68,8 @@ let build_dependent_inductive ind (mib,mip) =
extended_rel_list mip.mind_nrealargs_ctxt mib.mind_params_ctxt
@ extended_rel_list 0 realargs)
-let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn ~init:c s
-let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn ~init:c s
+let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
+let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s
let my_it_mkLambda_or_LetIn_name s c =
it_mkLambda_or_LetIn_name (Global.env()) c s
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c96024553f..d18b540de7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2221,11 +2221,11 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls =
in
(* Abstract by equalitites *)
let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
- let abseqs = it_mkProd_or_LetIn ~init:(lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in
+ let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in
(* Abstract by the "generalized" hypothesis. *)
let genarg = mkProd_or_LetIn (Name id, body, c) abseqs in
(* Abstract by the extension of the context *)
- let genctyp = it_mkProd_or_LetIn ~init:genarg ctx in
+ let genctyp = it_mkProd_or_LetIn genarg ctx in
(* The goal will become this product. *)
let genc = mkCast (mkMeta meta, DEFAULTcast, genctyp) in
(* Apply the old arguments giving the proper instantiation of the hyp *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 09:42:54 +0000