diff options
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 657367e36..367430d91 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -157,8 +157,8 @@ val unfold_option : val change : constr_pattern option -> change_arg -> clause -> tactic val pattern_option : - (occurrences * constr) list -> goal_location -> tactic -val reduce : red_expr -> clause -> tactic + (occurrences * constr) list -> goal_location -> unit Proofview.tactic +val reduce : red_expr -> clause -> unit Proofview.tactic val unfold_constr : global_reference -> unit Proofview.tactic (** {6 Modification of the local context. } *) |