From 180a39219f6987b63e7cc34500371d5ce03188c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 22 May 2014 14:10:54 +0200
Subject: Moving the "specialize" tactic out of the AST. Also removed an
 obsolete variant of it, accepting an additional integer.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 01e01ff858..eeba560d71 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -128,7 +128,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
       rec_flag * evars_flag * ('trm,'nam) induction_clause_list
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecompose of 'ind list * 'trm
-  | TacSpecialize of int option * 'trm with_bindings
 
   (* Automation tactics *)
   | TacTrivial of debug * 'trm list * string list option
-- 
cgit v1.2.3