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 +-
 printing/pptactic.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

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
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 1502884be7..e8ccd29c8a 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1380,8 +1380,8 @@ module Make
         pr_uconstr = pr_closed_glob_env env Evd.empty;
         pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
         pr_lconstr = pr_lconstr_env env Evd.empty;
-        pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
-        pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
+        pr_pattern = pr_constr_pattern_env env Evd.empty;
+        pr_lpattern = pr_lconstr_pattern_env env Evd.empty;
         pr_constant = pr_evaluable_reference_env env;
         pr_reference = pr_located pr_ltac_constant;
         pr_name = pr_id;
-- 
cgit v1.2.3