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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/eqschemes.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
2 files changed, 4 insertions, 4 deletions
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 *) |