From d0bc16d1a0626f4137797bbf0c91e972a0ff43ac Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 11:05:26 +0100
Subject: Moving the "clear" tactic to TACTIC EXTEND.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 33a96150c1..10c616627a 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -161,7 +161,6 @@ type 'a gen_atomic_tactic_expr =
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
 
   (* Context management *)
-  | TacClear of bool * 'nam list
   | TacClearBody of 'nam list
   | TacMove of 'nam * 'nam move_location
   | TacRename of ('nam *'nam) list
-- 
cgit v1.2.3