diff options
| author | Gaëtan Gilbert | 2020-08-24 13:34:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-25 16:15:18 +0200 |
| commit | 495466d20d53ca33adc69a4d9f6cceb8f30d8aad (patch) | |
| tree | 31c4c0b49defed84125a0bffa4a138b4f824c231 /tactics | |
| parent | a9a0307e2695e97143a8fc36ccdbfdd7de0c3820 (diff) | |
Deprecate intro_using
This is a footgun as it can refresh the name. Callers can still ignore
the generated name by doing `intro_using_then id (fun _ -> tclUNIT())`.
Diffstat (limited to 'tactics')
| -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 |