Remove double induction tactic

3 files changed, 0 insertions, 58 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 9a55cabc86..9e7843b2bb 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -19,7 +19,6 @@ open Tacmach.New
 open Tacticals.New
 open Clenv
 open Tactics
-open Proofview.Notations
 
 type branch_args = {
   branchnum  : int;         (* the branch number *)
@@ -28,8 +27,6 @@ type branch_args = {
                                true=assumption, false=let-in *)
   branchnames : Tactypes.intro_patterns}
 
-module NamedDecl = Context.Named.Declaration
-
 type elim_kind = Case of bool | Elim
 
 (* Find the right elimination suffix corresponding to the sort of the goal *)
@@ -217,52 +214,3 @@ let h_decompose l c = decompose_these c l
 let h_decompose_or = decompose_or
 
 let h_decompose_and = decompose_and
-
-(* The tactic Double performs a double induction *)
-
-let induction_trailer abs_i abs_j bargs =
-  tclTHEN
-    (tclDO (abs_j - abs_i) intro)
-    (onLastHypId
-       (fun id ->
-          Proofview.Goal.enter begin fun gl ->
-          let idty = pf_get_type_of gl (mkVar id) in
-          let fvty = global_vars (pf_env gl) (project gl) idty in
-          let possible_bring_hyps =
-            (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs
-          in
-          let (hyps,_) =
-            List.fold_left
-              (fun (bring_ids,leave_ids) d ->
-                 let cid = NamedDecl.get_id d in
-                 if not (List.mem cid leave_ids)
-                 then (d::bring_ids,leave_ids)
-                 else (bring_ids,cid::leave_ids))
-              ([],fvty) possible_bring_hyps
-          in
-          let ids = List.rev (ids_of_named_context hyps) in
-          (tclTHENLIST
-            [revert ids; elimination_then (fun _ -> tclIDTAC) id])
-          end
-          ))
-
-let double_ind h1 h2 =
-  Proofview.Goal.enter begin fun gl ->
-  let abs_i = depth_of_quantified_hypothesis true h1 gl in
-  let abs_j = depth_of_quantified_hypothesis true h2 gl in
-  let abs =
-    if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
-    if abs_i > abs_j then  Proofview.tclUNIT (abs_j,abs_i) else
-      let info = Exninfo.reify () in
-      tclZEROMSG ~info (Pp.str "Both hypotheses are the same.") in
-  abs >>= fun (abs_i,abs_j) ->
-  (tclTHEN (tclDO abs_i intro)
-     (onLastHypId
-        (fun id ->
-           elimination_then
-             (introElimAssumsThen (induction_trailer abs_i abs_j)) id)))
-  end
-
-let h_double_induction = double_ind
-
-
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 01053502e4..a603b472f7 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -21,4 +21,3 @@ val case_tac : bool -> or_and_intro_pattern option ->
 val h_decompose       : inductive list -> constr -> unit Proofview.tactic
 val h_decompose_or    : constr -> unit Proofview.tactic
 val h_decompose_and   : constr -> unit Proofview.tactic
-val h_double_induction : quantified_hypothesis -> quantified_hypothesis-> unit Proofview.tactic
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