From daa7cb065a238c7d4ee394e00315d66d023e5259 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Dec 2015 17:55:25 +0100
Subject: Removing auto from the tactic AST.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index ead221c5fb..aa1088c9ea 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -162,10 +162,6 @@ type 'a gen_atomic_tactic_expr =
       rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
 
-  (* Automation tactics *)
-  | TacTrivial of debug * 'trm list * string list option
-  | TacAuto of debug * int or_var option * 'trm list * string list option
-
   (* Context management *)
   | TacClear of bool * 'nam list
   | TacClearBody of 'nam list
-- 
cgit v1.2.3