From a1596ac8127071db6c507909bd9723edc720542d Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 27 Jun 2013 16:51:52 +0000
Subject: Getting rid of IntroPatternArgType.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 intf/tacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 86ac93d897..df4ed2c41e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -188,7 +188,6 @@ and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
   | MetaIdArg      of Loc.t * bool * string
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
-  | IntroPattern   of intro_pattern_expr located
   | Reference      of 'ref
   | TacCall of Loc.t * 'ref *
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg list
-- 
cgit v1.2.3