aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/genintern.ml8
-rw-r--r--interp/genintern.mli8
-rw-r--r--interp/stdarg.ml13
-rw-r--r--interp/stdarg.mli23
-rw-r--r--plugins/funind/g_indfun.ml41
-rw-r--r--plugins/ltac/coretactics.ml41
-rw-r--r--plugins/ltac/extraargs.ml42
-rw-r--r--plugins/ltac/g_ltac.ml42
-rw-r--r--plugins/ltac/tacarg.ml8
-rw-r--r--plugins/ltac/tacarg.mli26
-rw-r--r--plugins/ltac/taccoerce.ml1
-rw-r--r--plugins/ltac/tacexpr.ml2
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--proofs/tactypes.ml (renamed from interp/tactypes.ml)8
14 files changed, 55 insertions, 50 deletions
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 161201c44..d9a0db040 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -26,9 +26,15 @@ let empty_glob_sign env = {
extra = Store.empty;
}
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+ in the environment by the effective calls to Intro, Inversion, etc
+ The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
+
type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
type 'glb subst_fun = substitution -> 'glb -> 'glb
-type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
module InternObj =
struct
diff --git a/interp/genintern.mli b/interp/genintern.mli
index d818713fc..f4f064bca 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -22,6 +22,12 @@ type glob_sign = {
val empty_glob_sign : Environ.env -> glob_sign
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+ in the environment by the effective calls to Intro, Inversion, etc
+ The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
+
(** {5 Internalization functions} *)
type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
@@ -42,7 +48,7 @@ val generic_substitute : glob_generic_argument subst_fun
(** {5 Notation functions} *)
-type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index e5ed58be6..7a7bb9a84 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -34,9 +34,6 @@ let wit_pre_ident : string uniform_genarg_type =
let wit_int_or_var =
make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
-let wit_intro_pattern =
- make0 "intropattern"
-
let wit_ident =
make0 "ident"
@@ -45,8 +42,6 @@ let wit_var =
let wit_ref = make0 "ref"
-let wit_quant_hyp = make0 "quant_hyp"
-
let wit_sort_family = make0 "sort_family"
let wit_constr =
@@ -56,12 +51,6 @@ let wit_uconstr = make0 "uconstr"
let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
-let wit_constr_with_bindings = make0 "constr_with_bindings"
-
-let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
-
-let wit_bindings = make0 "bindings"
-
let wit_red_expr = make0 "redexpr"
let wit_clause_dft_concl =
@@ -74,6 +63,4 @@ let wit_preident = wit_pre_ident
let wit_reference = wit_ref
let wit_global = wit_ref
let wit_clause = wit_clause_dft_concl
-let wit_quantified_hypothesis = wit_quant_hyp
-let wit_intropattern = wit_intro_pattern
let wit_redexpr = wit_red_expr
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index dc9c370a1..4159e6054 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -18,8 +18,8 @@ open Genredexpr
open Pattern
open Constrexpr
open Misctypes
-open Tactypes
open Genarg
+open Genintern
val wit_unit : unit uniform_genarg_type
@@ -35,16 +35,12 @@ val wit_pre_ident : string uniform_genarg_type
val wit_int_or_var : (int or_var, int or_var, int) genarg_type
-val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
-
val wit_ident : Id.t uniform_genarg_type
val wit_var : (lident, lident, Id.t) genarg_type
val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
-val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-
val wit_sort_family : (Sorts.family, unit, unit) genarg_type
val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
@@ -54,21 +50,6 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_
val wit_open_constr :
(constr_expr, glob_constr_and_expr, constr) genarg_type
-val wit_constr_with_bindings :
- (constr_expr with_bindings,
- glob_constr_and_expr with_bindings,
- constr with_bindings delayed_open) genarg_type
-
-val wit_open_constr_with_bindings :
- (constr_expr with_bindings,
- glob_constr_and_expr with_bindings,
- constr with_bindings delayed_open) genarg_type
-
-val wit_bindings :
- (constr_expr bindings,
- glob_constr_and_expr bindings,
- constr bindings delayed_open) genarg_type
-
val wit_red_expr :
((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
(glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
@@ -83,8 +64,6 @@ val wit_preident : string uniform_genarg_type
val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
-val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
-val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
val wit_redexpr :
((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
(glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 24d1a40c2..9899b7b21 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -15,6 +15,7 @@ open Indfun_common
open Indfun
open Genarg
open Stdarg
+open Tacarg
open Tactypes
open Pcoq
open Pcoq.Prim
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 1070b30a1..8f59559eb 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -15,6 +15,7 @@ open Tactypes
open Genredexpr
open Stdarg
open Extraargs
+open Tacarg
open Names
open Logic
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 4e7c8b754..ddc157cac 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -35,7 +35,7 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr
-let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Stdarg.wit_intro_pattern
+let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern
let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
let () =
let inject (loc, v) = Tacexpr.Tacexp v in
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index de9ff2875..c39192d46 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -36,7 +36,7 @@ let arg_of_expr = function
let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
-let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat
+let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat
let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 6eb482b1c..8a25d4851 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -19,6 +19,14 @@ let make0 ?dyn name =
let () = Geninterp.register_val0 wit dyn in
wit
+let wit_intro_pattern = make0 "intropattern"
+let wit_quant_hyp = make0 "quant_hyp"
+let wit_constr_with_bindings = make0 "constr_with_bindings"
+let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
+let wit_bindings = make0 "bindings"
+let wit_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+
let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
make0 "tactic"
diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index 1abe7cd6f..bdb0be03c 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -9,9 +9,33 @@
(************************************************************************)
open Genarg
-open Tacexpr
+open EConstr
open Constrexpr
open Tactypes
+open Tacexpr
+
+(** Tactic related witnesses, could also live in tactics/ if other users *)
+val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
+
+val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
+
+val wit_constr_with_bindings :
+ (constr_expr with_bindings,
+ glob_constr_and_expr with_bindings,
+ constr with_bindings delayed_open) genarg_type
+
+val wit_open_constr_with_bindings :
+ (constr_expr with_bindings,
+ glob_constr_and_expr with_bindings,
+ constr with_bindings delayed_open) genarg_type
+
+val wit_bindings :
+ (constr_expr bindings,
+ glob_constr_and_expr bindings,
+ constr bindings delayed_open) genarg_type
+
+val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
(** Generic arguments based on Ltac. *)
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 27acbb629..6bfa07ee9 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -17,6 +17,7 @@ open Namegen
open Tactypes
open Genarg
open Stdarg
+open Tacarg
open Geninterp
open Pp
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 289434d8a..f4dd85bc2 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -118,7 +118,7 @@ type ml_tactic_entry = {
(** Composite types *)
-type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+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
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 42f6883b4..be07654ef 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -118,7 +118,7 @@ type ml_tactic_entry = {
(** Composite types *)
-type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+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
diff --git a/interp/tactypes.ml b/proofs/tactypes.ml
index f19abefee..86a7e9c52 100644
--- a/interp/tactypes.ml
+++ b/proofs/tactypes.ml
@@ -13,8 +13,6 @@
meant to stay. *)
open Names
-open Constrexpr
-open Pattern
(** Introduction patterns *)
@@ -45,12 +43,6 @@ type 'a bindings =
type 'a with_bindings = 'a * 'a bindings
-(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
- in the environment by the effective calls to Intro, Inversion, etc
- The [constr_expr] field is [None] in TacDef though *)
-type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
-type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern
-
type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
type delayed_open_constr = EConstr.constr delayed_open
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 06:49:45 +0000