diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-04-10 18:28:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-04-10 18:28:12 +0200 |
| commit | a86ae4d352cc8e4ac306f04d5536d7fff04d3303 (patch) | |
| tree | bf7aa3e7cdf5be6f68a1c8784ec53ce9d93f1e5c /tactics/tactics.mli | |
| parent | 07d63e1333dc73eda3e49e904ff8df6e7f62fa79 (diff) | |
Fix #3590 for good this time, by changing the API, change's argument now
takes a variable substitution for matched variables in the (lhs) pattern, and
uses the existing ist structure to pretype the rhs correcly, without
having to deal with the volatile evars.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index eea495621..0069d100b 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -125,8 +125,9 @@ val exact_proof : Constrexpr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr -type change_arg = evar_map -> evar_map * constr +type change_arg = patvar_map -> evar_map -> evar_map * constr +val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> tactic val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic val reduct_in_concl : tactic_reduction * cast_kind -> tactic |