Removing "double induction" from the tactic AST.

7 files changed, 7 insertions, 20 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index e06436d8a3..4fe60538a4 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -157,7 +157,6 @@ type 'a gen_atomic_tactic_expr =
   (* Derived basic tactics *)
   | TacInductionDestruct of
       rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
-  | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
 
   (* Context management *)
   | TacRename of ('nam *'nam) list
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index ce28eacc09..63b5463c49 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -222,6 +222,13 @@ TACTIC EXTEND simple_destruct
   [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ]
 END
 
+(** Double induction *)
+
+TACTIC EXTEND double_induction
+  [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
+  [ Elim.h_double_induction h1 h2 ]
+END
+
 (* Admit *)
 
 TACTIC EXTEND admit
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 3744449e97..0f827755a6 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -520,10 +520,6 @@ let rec intern_atomic lf ist x =
                Option.map (intern_or_and_intro_pattern_loc lf ist) ipats),
                Option.map (clause_app (intern_hyp_location ist)) cls)) l,
                Option.map (intern_constr_with_bindings ist) el))
-  | TacDoubleInduction (h1,h2) ->
-      let h1 = intern_quantified_hypothesis ist h1 in
-      let h2 = intern_quantified_hypothesis ist h2 in
-      TacDoubleInduction (h1,h2)
   (* Context management *)
   | TacRename l ->
       TacRename (List.map (fun (id1,id2) ->
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index fcc29a8302..f6f988ee23 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1822,12 +1822,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
-  | TacDoubleInduction (h1,h2) ->
-      let h1 = interp_quantified_hypothesis ist h1 in
-      let h2 = interp_quantified_hypothesis ist h2 in
-      name_atomic
-        (TacDoubleInduction (h1,h2))
-        (Elim.h_double_induction h1 h2)
   (* Context management *)
   | TacRename l ->
       Proofview.Goal.enter { enter = begin fun gl ->
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 3f504b7f37..71dd718e87 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -162,7 +162,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
         subst_induction_arg subst c, ids, cls) l in
       let el' = Option.map (subst_glob_with_bindings subst) el in
       TacInductionDestruct (isrec,ev,(l',el'))
-  | TacDoubleInduction (h1,h2) as x -> x
 
   (* Context management *)
   | TacRename l as x -> x
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index cfe5377d63..9f19817ddf 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -606,8 +606,6 @@ GEXTEND Gram
 	  TacAtom (!@loc, TacInductionDestruct (true,false,ic))
       | IDENT "einduction"; ic = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct(true,true,ic))
-      | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
-	  h2 = quantified_hypothesis -> TacAtom (!@loc, TacDoubleInduction (h1,h2))
       | IDENT "destruct"; icl = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct(false,false,icl))
       | IDENT "edestruct";  icl = induction_clause_list ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 44c832bd7a..5192e2db12 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -909,12 +909,6 @@ module Make
                 pr_opt (pr_clauses None pr.pr_name) cl) l ++
               pr_opt pr_eliminator el
           )
-        | TacDoubleInduction (h1,h2) ->
-          hov 1 (
-            primitive "double induction"
-            ++ pr_arg pr_quantified_hypothesis h1
-            ++ pr_arg pr_quantified_hypothesis h2
-          )
 
         (* Context management *)
         | TacRename l ->