diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-01 22:54:24 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-02 11:19:08 +0100 |
| commit | 767816eece27e6bb8cba0bbf122507bd2a3b77a1 (patch) | |
| tree | 6348c7ac8f50e4782a41072e5db26d83b3b1a3a5 /plugins/ltac/pptactic.mli | |
| parent | 0df9c751f98d2f9b4423eb1bee17730cd0bf0123 (diff) | |
Using a specific function to register vernac printers.
Diffstat (limited to 'plugins/ltac/pptactic.mli')
| -rw-r--r-- | plugins/ltac/pptactic.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 058b20569..b47f07a45 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -46,6 +46,10 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit +val declare_extra_vernac_genarg_pprule : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer -> unit + type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list type pp_tactic = { |