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/functional_principles_proofs.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/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 12 |
1 files changed, 6 insertions, 6 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 |