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/tactics.mli | |
| parent | 49e9fe1c4666beda099872988144d12138dc6349 (diff) | |
Fixes #8553 (regression of tactic "change" under binders).
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |