From 1d6eac66b4f21a768e98d01416e4ecef68ada377 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 1 Sep 2014 16:54:53 +0200
Subject: Moving the decompose tactic out of 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 abb2292cd1..261c28d7f3 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -144,7 +144,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacInductionDestruct of
       rec_flag * evars_flag * ('trm,'nam) induction_clause_list
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
-  | TacDecompose of 'ind list * 'trm
 
   (* Automation tactics *)
   | TacTrivial of debug * 'trm list * string list option
-- 
cgit v1.2.3