diff options
| author | Hugo Herbelin | 2018-09-25 12:58:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 13:27:10 +0200 |
| commit | 802f5513983080884971b3d9c7ed0cc3ee76c404 (patch) | |
| tree | 56d3f653683d69d77763424c19a785395dced3f3 /tactics | |
| parent | 49e9fe1c4666beda099872988144d12138dc6349 (diff) | |
Fixes #8553 (regression of tactic "change" under binders).
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6999b17d8e..f3f81ff616 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -791,9 +791,9 @@ let e_change_in_hyp redfun (id,where) = (convert_hyp c) end -type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr +type change_arg = Ltac_pretype.patvar_map -> env -> evar_map -> evar_map * EConstr.constr -let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c) +let make_change_arg c pats env sigma = (sigma, replace_vars (Id.Map.bindings pats) c) let check_types env sigma mayneedglobalcheck deep newc origc = let t1 = Retyping.get_type_of env sigma newc in @@ -818,7 +818,7 @@ let check_types env sigma mayneedglobalcheck deep newc origc = (* Now we introduce different instances of the previous tacticals *) let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = - let (sigma, t') = t sigma in + let (sigma, t') = t env sigma in let sigma = check_types env sigma mayneedglobalcheck deep t' c in match infer_conv ~pb:cv_pb env sigma t' c with | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible."); diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c088e404b0..24c12ffd82 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -145,7 +145,7 @@ val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic type tactic_reduction = Reductionops.reduction_function type e_tactic_reduction = Reductionops.e_reduction_function -type change_arg = patvar_map -> evar_map -> evar_map * constr +type change_arg = patvar_map -> env -> evar_map -> evar_map * constr val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic |