From e321cfd21e28161923b84d943cb15c6d775b0d9e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 16 May 2014 17:01:42 +0200
Subject: Moving argument-free tactics out of the AST into a dedicated
 "coretactics.ml4" file.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 16b1dc5eb1..532786fd37 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -105,7 +105,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacIntroPattern of intro_pattern_expr located list
   | TacIntrosUntil of quantified_hypothesis
   | TacIntroMove of Id.t option * 'nam move_location
-  | TacAssumption
   | TacExact of 'trm
   | TacExactNoCheck of 'trm
   | TacVmCastNoCheck of 'trm
@@ -163,7 +162,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacChange of 'pat option * 'trm * 'nam clause_expr
 
   (* Equivalence relations *)
-  | TacReflexivity
   | TacSymmetry of 'nam clause_expr
   | TacTransitivity of 'trm option
 
-- 
cgit v1.2.3