From 2c01bd7b446c1151922ad0a01c3dc6b85f5bea54 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 Apr 2016 19:27:30 +0200
Subject: Removing "double induction" from the tactic AST.

---
 intf/tacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

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