aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/genintern.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-13 10:25:20 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-13 10:25:20 +0200
commitc1d690443589a457b18b39b7003ccb762bcf401f (patch)
tree723f70ee85dc2b646ea19d8afa03972d21c78820 /interp/genintern.mli
parent573c6d76d343cadaa68b5851fdebba937153c24d (diff)
parent1dd682b1cafd64dd902e1ae6ea738192eb9b26db (diff)
Merge PR #7677: [api] Remove Misctypes
Diffstat (limited to 'interp/genintern.mli')
-rw-r--r--interp/genintern.mli8
1 files changed, 7 insertions, 1 deletions
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