From e705ae9d343c67212ce238899d21059ce93ee3e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 18 May 2014 02:50:51 +0200
Subject: Tentative to add constr-using primitive tactics without grammar
 rules. We eta-expand primitive Ltac functions, and instead of feeding
 TacExtend directly with its arguments, we use the environment to retrieve
 them.

Some tactics from the AST were also moved away and made using this
mechanism.
---
 intf/tacexpr.mli | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 532786fd37..5a7a20ef63 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -106,19 +106,14 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacIntrosUntil of quantified_hypothesis
   | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
-  | TacExactNoCheck of 'trm
-  | TacVmCastNoCheck of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings list *
       ('nam * intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings * 'trm with_bindings option
-  | TacElimType of 'trm
   | TacCase of evars_flag * 'trm with_bindings
-  | TacCaseType of 'trm
   | TacFix of Id.t option * int
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacCofix of Id.t option
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
-  | TacCut of 'trm
   | TacAssert of
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option *
       intro_pattern_expr located option * 'trm
@@ -136,7 +131,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacDecomposeOr of 'trm
   | TacDecompose of 'ind list * 'trm
   | TacSpecialize of int option * 'trm with_bindings
-  | TacLApply of 'trm
 
   (* Automation tactics *)
   | TacTrivial of debug * 'trm list * string list option
-- 
cgit v1.2.3