diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-22 04:57:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
| commit | 18aac5cdc6ce8be8c5c88d284cd10e82814cb303 (patch) | |
| tree | cd73ab17e32bbe46c422208469c912f87968fc47 /interp/genintern.mli | |
| parent | 368a25e4ef14512b00f5799e26c3f615bc540201 (diff) | |
[api] Misctypes removal: move Tactypes to proofs
This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.
Diffstat (limited to 'interp/genintern.mli')
| -rw-r--r-- | interp/genintern.mli | 8 |
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 |