From b8de2bae178a63a6c482a46ee01e5183676984ee Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 28 Nov 2018 02:33:37 +0100
Subject: [ltac] Remove aliases already present in the lower layers.

We remove a few aliases present in the lower layers
[`Genintern/Tactypes`] from `Tacexpr`.

IMHO this enlarges the API for no good purpose, and difficults
analysis.
---
 plugins/ssrmatching/ssrmatching.ml  | 2 +-
 plugins/ssrmatching/ssrmatching.mli | 4 +---
 2 files changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins/ssrmatching')

diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 8cb0a8b463..6497b6ff98 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -896,7 +896,7 @@ let interp_rpattern s = function
 
 let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t
 
-type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option
+type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option
 let tag_of_cpattern = pi1
 let loc_of_cpattern = loc_ofCG
 let cpattern_of_term (c, t) ist = c, t, Some ist
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 93a8c48435..8672c55767 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -5,9 +5,7 @@ open Goal
 open Environ
 open Evd
 open Constr
-
-open Ltac_plugin
-open Tacexpr
+open Genintern
 
 (** ******** Small Scale Reflection pattern matching facilities ************* *)
 
-- 
cgit v1.2.3