diff options
| author | Pierre-Marie Pédrot | 2016-09-14 18:26:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-15 13:02:43 +0200 |
| commit | 404a8c619f76c572aec65f413baf087a374b37c3 (patch) | |
| tree | fae62d94ddd348695c43625308d1bc46cf294be6 /interp/genintern.mli | |
| parent | 699b70cd9ad0d79cbde228bdb51fde224a3b524e (diff) | |
Generalizing the notion of constr substitution to generic arguments.
This removes a dependency on wit_tactic in Constrintern.
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 4b244b38d8..aabb85e009 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 |