diff options
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 *) |