Remove double induction tactic

1 files changed, 0 insertions, 5 deletions

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a6471be549..9fd50cf0c2 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -81,11 +81,6 @@ val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic
 
 val intros               : unit Proofview.tactic
 
-(** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
-   the conclusion of goal [g], up to head-reduction if [b] is [true] *)
-val depth_of_quantified_hypothesis :
-  bool -> quantified_hypothesis -> Proofview.Goal.t -> int
-
 val intros_until         : quantified_hypothesis -> unit Proofview.tactic
 
 val intros_clearing      : bool list -> unit Proofview.tactic