From 53dc6613499ca18672cda02697f182eb97cda8dc Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 25 Jun 2015 15:24:55 +0200
Subject: Remove other types not carried by interpretations in `Tacexpr`.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 91e020586b..86714ca4d5 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -386,7 +386,7 @@ type raw_tactic_arg =
 
 type t_trm = Term.constr
 type t_utrm = Glob_term.closed_glob_constr
-type t_pat = glob_constr_and_expr * constr_pattern
+type t_pat = constr_pattern
 type t_cst = evaluable_global_reference
 type t_ref = ltac_constant located
 type t_nam  = Id.t
-- 
cgit v1.2.3