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/ssr/ssrast.mli    | 2 +-
 plugins/ssr/ssrcommon.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index a786b9953d..bb8a0faf2e 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -47,7 +47,7 @@ type ssrdocc = ssrclear option * ssrocc
 
 (* OLD ssr terms *)
 type ssrtermkind = char (* FIXME, make algebraic *)
-type ssrterm = ssrtermkind * Tacexpr.glob_constr_and_expr
+type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
 
 (* NEW ssr term *)
 
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index e25c93bf0a..824827e90c 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -146,7 +146,7 @@ val interp_refine :
 
 val interp_open_constr :
   Tacinterp.interp_sign -> Goal.goal Evd.sigma ->
-    Tacexpr.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t)
+    Genintern.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t)
 
 val pf_e_type_of :
   Goal.goal Evd.sigma ->
-- 
cgit v1.2.3