diff options
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.mli | 3 |
2 files changed, 7 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 70cea89ccb..eb7b7e363f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1068,6 +1068,10 @@ let rec intros_using = function | [] -> Proofview.tclUNIT() | str::l -> Tacticals.New.tclTHEN (intro_using str) (intros_using l) +let rec intros_mustbe_force = function + | [] -> Proofview.tclUNIT() + | str::l -> Tacticals.New.tclTHEN (intro_mustbe_force str) (intros_mustbe_force l) + let rec intros_using_then_helper tac acc = function | [] -> tac (List.rev acc) | str::l -> intro_using_then str (fun str' -> intros_using_then_helper tac (str'::acc) l) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 00739306a7..54c781af5c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -65,10 +65,13 @@ val intro_avoiding : Id.Set.t -> unit Proofview.tactic val intro_replacing : Id.t -> unit Proofview.tactic val intro_using : Id.t -> unit Proofview.tactic +[@@ocaml.deprecated "Prefer [intro_using_then] to avoid renaming issues."] val intro_using_then : Id.t -> (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intro_mustbe_force : Id.t -> unit Proofview.tactic +val intros_mustbe_force : Id.t list -> unit Proofview.tactic val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intros_using : Id.t list -> unit Proofview.tactic +[@@ocaml.deprecated "Prefer [intros_using_then] to avoid renaming issues."] val intros_using_then : Id.t list -> (Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic val intros_replacing : Id.t list -> unit Proofview.tactic val intros_possibly_replacing : Id.t list -> unit Proofview.tactic |