diff options
| author | Pierre-Marie Pédrot | 2019-04-23 18:39:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-24 13:44:35 +0200 |
| commit | db72bf79423fc17a3eecdfd559736bb887936cc6 (patch) | |
| tree | 7b10bf92e807d0a06f3e293a956ee287ef85ddea /tactics/tactics.mli | |
| parent | d54d63adfd9bd399ca5c31d77977c81887a2e4f0 (diff) | |
Code factorization in conversion tactics.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index e545ec9b5f..e7b95a820e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -154,8 +154,8 @@ 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 val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic -val reduct_in_concl : tactic_reduction * cast_kind -> unit Proofview.tactic -val e_reduct_in_concl : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic +val reduct_in_concl : ?check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic +val e_reduct_in_concl : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic val change_concl : constr -> unit Proofview.tactic val change_in_hyp : (occurrences * constr_pattern) option -> change_arg -> |