diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 12 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 16 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 8 |
3 files changed, 17 insertions, 19 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 |