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/ltac/extraargs.mli | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac/extraargs.mli')

diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index fa70235975..0509d6ae71 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Genintern
 open Tacexpr
 open Names
 open Constrexpr
@@ -28,22 +29,22 @@ val wit_natural : int Genarg.uniform_genarg_type
 
 val wit_glob :
   (constr_expr,
-  Tacexpr.glob_constr_and_expr,
+  glob_constr_and_expr,
   Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
 
 val wit_lglob :
   (constr_expr,
-  Tacexpr.glob_constr_and_expr,
+  glob_constr_and_expr,
   Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
 
 val wit_lconstr :
   (constr_expr,
-  Tacexpr.glob_constr_and_expr,
+  glob_constr_and_expr,
   EConstr.t) Genarg.genarg_type
 
 val wit_casted_constr :
   (constr_expr,
-  Tacexpr.glob_constr_and_expr,
+  glob_constr_and_expr,
   EConstr.t) Genarg.genarg_type
 
 val glob : constr_expr Pcoq.Entry.t
-- 
cgit v1.2.3