aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh6
-rw-r--r--plugins/ltac/extraargs.mli9
-rw-r--r--plugins/ltac/extratactics.mli2
-rw-r--r--plugins/ltac/g_rewrite.mlg7
-rw-r--r--plugins/ltac/pptactic.ml1
-rw-r--r--plugins/ltac/pptactic.mli1
-rw-r--r--plugins/ltac/rewrite.mli1
-rw-r--r--plugins/ltac/tacarg.mli1
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacexpr.ml17
-rw-r--r--plugins/ltac/tacexpr.mli18
-rw-r--r--plugins/ltac/tacintern.mli1
-rw-r--r--plugins/ltac/tacinterp.mli2
-rw-r--r--plugins/ltac/tacsubst.mli1
-rw-r--r--plugins/ltac/tactic_debug.mli2
-rw-r--r--plugins/ltac/tactic_matching.mli4
-rw-r--r--plugins/ssr/ssrast.mli2
-rw-r--r--plugins/ssr/ssrcommon.mli2
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
-rw-r--r--plugins/ssrmatching/ssrmatching.mli4
20 files changed, 38 insertions, 47 deletions
diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
new file mode 100644
index 0000000000..2df8affd14
--- /dev/null
+++ b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then
+
+ elpi_CI_REF=ltac+remove_aliases
+ elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+fi
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
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 ->
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 ************* *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:35:37 +0000