From b600c51753c5b60e62bdfcf1e6409afa1ce69d7a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Aug 2014 01:10:26 +0200
Subject: Removing "intros untils" from the AST.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 0c5eed7144..7f7ecdcf77 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -111,7 +111,6 @@ type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of intro_pattern_expr located list
-  | TacIntrosUntil of quantified_hypothesis
   | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
-- 
cgit v1.2.3