diff options
| author | glondu | 2010-09-28 15:32:01 +0000 |
|---|---|---|
| committer | glondu | 2010-09-28 15:32:01 +0000 |
| commit | 86919192359dee7e274ab4af17bd32efe11a5f44 (patch) | |
| tree | d09d9174894559ce1f34b078e3ae163e9e09515d /plugins/funind/invfun.ml | |
| parent | 013bc34fd828a5eb4eacd721a8021b64abf8a822 (diff) | |
Remove "init" label from Termops.it_mk* specialized functions
These functions are applied much more often without labels than with
them (the alternate of adding the label wherever relevant changes 124
lines instead of 41). Moreover, this is more consistent with the Term
module and there is no ambiguity in argument types. This commit goes
towards elimination of occurrences of OCaml warning 6.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13468 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |