From cd17f9bfad72fb8f8da486facd75ff8ceecebd24 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 19 Jan 2021 11:19:33 -0800
Subject: Remove double induction tactic

---
 tactics/tactics.mli | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'tactics/tactics.mli')

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