From 876f202985d5bd463bd5b44c195b239bcfedad7c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 7 Aug 2014 01:43:37 +0200
Subject: Removing simple induction / destruct from the AST.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 88e5c36961..8e5b51b873 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -130,7 +130,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
       intro_pattern_expr located option
 
   (* Derived basic tactics *)
-  | TacSimpleInductionDestruct of rec_flag * quantified_hypothesis
   | TacInductionDestruct of
       rec_flag * evars_flag * ('trm,'nam) induction_clause_list
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
-- 
cgit v1.2.3