diff options
Diffstat (limited to 'interp/genintern.mli')
| -rw-r--r-- | interp/genintern.mli | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/interp/genintern.mli b/interp/genintern.mli index 4b244b38d..aabb85e00 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -32,6 +32,14 @@ val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun val generic_substitute : glob_generic_argument subst_fun +(** {5 Notation functions} *) + +type 'glb ntn_subst_fun = Tacexpr.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb + +val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun + +val generic_substitute_notation : glob_generic_argument ntn_subst_fun + (** Registering functions *) val register_intern0 : ('raw, 'glb, 'top) genarg_type -> @@ -39,3 +47,6 @@ val register_intern0 : ('raw, 'glb, 'top) genarg_type -> val register_subst0 : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun -> unit + +val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type -> + 'glb ntn_subst_fun -> unit |