[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.

15 files changed, 28 insertions, 41 deletions

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
diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli
index 7fb9a19a0c..4576562634 100644
--- a/plugins/ltac/extratactics.mli
+++ b/plugins/ltac/extratactics.mli
@@ -14,4 +14,4 @@ val injHyp : Names.Id.t -> unit Proofview.tactic
 
 (* val refine_tac : Evd.open_constr -> unit Proofview.tactic *)
 
-val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tacexpr.delayed_open option -> unit Proofview.tactic
+val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tactypes.delayed_open option -> unit Proofview.tactic
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index f7375a0f01..31fb1c9abf 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -16,6 +16,7 @@ open Names
 open Locus
 open Constrexpr
 open Glob_term
+open Genintern
 open Geninterp
 open Extraargs
 open Tacmach
@@ -37,8 +38,8 @@ DECLARE PLUGIN "ltac_plugin"
 {
 
 type constr_expr_with_bindings = constr_expr with_bindings
-type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
-type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings
+type glob_constr_with_bindings = glob_constr_and_expr with_bindings
+type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings
 
 let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) =
   let _, env = Pfedit.get_current_context () in
@@ -70,7 +71,7 @@ END
 {
 
 type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast
-type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
+type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
 
 let interp_strategy ist gl s = 
   let sigma = project gl in
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 50cfb6d004..55e58187b0 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -26,6 +26,7 @@ open Pputils
 open Ppconstr
 open Printer
 
+open Genintern
 open Tacexpr
 open Tacarg
 open Tactics
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 6c09e447a5..0ab9e501bc 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -17,6 +17,7 @@ open Names
 open Environ
 open Constrexpr
 open Notation_gram
+open Genintern
 open Tacexpr
 open Tactypes
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 4f46e78c71..2457b265f0 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -13,6 +13,7 @@ open Environ
 open EConstr
 open Constrexpr
 open Evd
+open Genintern
 open Tactypes
 open Tacexpr
 open Tacinterp
diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index bdb0be03cf..0c7096a4de 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -11,6 +11,7 @@
 open Genarg
 open EConstr
 open Constrexpr
+open Genintern
 open Tactypes
 open Tacexpr
 
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index d2ae92f6ce..b04c3b9f4e 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -53,7 +53,7 @@ val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t
 
 val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Id.t
 
-val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
+val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> delayed_open_constr intro_pattern_expr
 
 val coerce_to_intro_pattern_naming :
   Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 9435d0b911..2bd21f9d7a 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -93,19 +93,8 @@ type ml_tactic_entry = {
 
 (** Composite types *)
 
-type glob_constr_and_expr = Genintern.glob_constr_and_expr
-
 type open_constr_expr = unit * constr_expr
-type open_glob_constr = unit * glob_constr_and_expr
-
-type binding_bound_vars = Constr_matching.binding_bound_vars
-type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern
-
-type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
-
-type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
-
-type delayed_open_constr = EConstr.constr delayed_open
+type open_glob_constr = unit * Genintern.glob_constr_and_expr
 
 type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
 type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
@@ -279,8 +268,8 @@ constraint 'a = <
 
 (** Globalized tactics *)
 
-type g_trm = glob_constr_and_expr
-type g_pat = glob_constr_pattern_and_expr
+type g_trm = Genintern.glob_constr_and_expr
+type g_pat = Genintern.glob_constr_pattern_and_expr
 type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 1527724420..0c27f3bfe2 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -92,20 +92,8 @@ type ml_tactic_entry = {
 }
 
 (** Composite types *)
-
-type glob_constr_and_expr = Genintern.glob_constr_and_expr
-
 type open_constr_expr = unit * constr_expr
-type open_glob_constr = unit * glob_constr_and_expr
-
-type binding_bound_vars = Constr_matching.binding_bound_vars
-type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern
-
-type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
-
-type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
-
-type delayed_open_constr = EConstr.constr delayed_open
+type open_glob_constr = unit * Genintern.glob_constr_and_expr
 
 type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
 type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
@@ -279,8 +267,8 @@ constraint 'a = <
 
 (** Globalized tactics *)
 
-type g_trm = glob_constr_and_expr
-type g_pat = glob_constr_pattern_and_expr
+type g_trm = Genintern.glob_constr_and_expr
+type g_pat = Genintern.glob_constr_pattern_and_expr
 type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 178f6af71d..978ad4dd24 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -12,6 +12,7 @@ open Names
 open Tacexpr
 open Genarg
 open Constrexpr
+open Genintern
 open Tactypes
 
 (** Globalization of tactic expressions :
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index f9883e4441..d9c80bb835 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -43,6 +43,8 @@ type interp_sign = Geninterp.interp_sign = {
   lfun : value Id.Map.t;
   extra : TacStore.t }
 
+open Genintern
+
 val f_avoid_ids : Id.Set.t TacStore.field
 val f_debug : debug_info TacStore.field
 
diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index d406686c56..4487604dca 100644
--- a/plugins/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
@@ -11,6 +11,7 @@
 open Tacexpr
 open Mod_subst
 open Genarg
+open Genintern
 open Tactypes
 
 (** Substitution of tactics at module closing time *)
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 175341df09..91e8510b92 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -40,7 +40,7 @@ val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLog
 
 (** Prints the pattern rule *)
 val db_pattern_rule :
-  debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t
+  debug_info -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t
 
 (** Prints a matched hypothesis *)
 val db_matched_hyp :
diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli
index 0722c68783..457c4e0b9a 100644
--- a/plugins/ltac/tactic_matching.mli
+++ b/plugins/ltac/tactic_matching.mli
@@ -35,7 +35,7 @@ val match_term :
   Environ.env ->
   Evd.evar_map ->
   EConstr.constr ->
-  (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+  (Constr_matching.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic
 
 (** [match_goal env sigma hyps concl rules] matches the goal
@@ -48,5 +48,5 @@ val match_goal:
   Evd.evar_map ->
   EConstr.named_context ->
   EConstr.constr ->
-  (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+  (Constr_matching.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic