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 2202fa8c8..b894628c3 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -359,8 +359,8 @@ val intros_transitivity : constr option -> tactic val cut : constr -> tactic val cut_intro : constr -> tactic -val cut_replacing : - identifier -> constr -> (tactic -> tactic) -> tactic +val assert_replacing : identifier -> types -> tactic -> tactic +val cut_replacing : identifier -> types -> tactic -> tactic val cut_in_parallel : constr list -> tactic val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic |