From 495466d20d53ca33adc69a4d9f6cceb8f30d8aad Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 24 Aug 2020 13:34:47 +0200
Subject: 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())`.
---
 tactics/tactics.ml  | 4 ++++
 tactics/tactics.mli | 3 +++
 2 files changed, 7 insertions(+)

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
-- 
cgit v1.2.3