diff options
| author | Pierre-Marie Pédrot | 2015-10-29 20:04:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-29 20:25:02 +0100 |
| commit | bf1eef119ef8f0e6a2ae4b66165d6e22c1ce9236 (patch) | |
| tree | eae73dd080b6a704922c3ffcf7b47ede9e13651f /tactics/tactics.mli | |
| parent | 4afb91237fa89fd9dc018a567382e34d6b1e616f (diff) | |
Monotonizing Tactics.change_arg.
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 d62d27ca34..8a4717b7ba 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -125,7 +125,7 @@ val exact_proof : Constrexpr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr -type change_arg = patvar_map -> evar_map -> evar_map * constr +type change_arg = patvar_map -> constr Sigma.run val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> tactic |