diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 10 | ||||
| -rw-r--r-- | printing/pptactic.mli | 9 |
2 files changed, 15 insertions, 4 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index d16035fba0..b790c4ea68 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -28,11 +28,17 @@ let pr_global x = Nametab.pr_global_env Idset.empty x type grammar_terminals = string option list +type pp_tactic = { + pptac_key : string; + pptac_args : argument_type list; + pptac_prods : int * grammar_terminals; +} + (* Extensions *) let prtac_tab = Hashtbl.create 17 -let declare_extra_tactic_pprule (s,tags,prods) = - Hashtbl.add prtac_tab (s,tags) prods +let declare_extra_tactic_pprule pt = + Hashtbl.add prtac_tab (pt.pptac_key, pt.pptac_args) (pt.pptac_prods) let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags) diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 249a4a0afb..61acffd081 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -47,9 +47,14 @@ val declare_extra_genarg_pprule : type grammar_terminals = string option list +type pp_tactic = { + pptac_key : string; + pptac_args : argument_type list; + pptac_prods : int * grammar_terminals; +} + (** if the boolean is false then the extension applies only to old syntax *) -val declare_extra_tactic_pprule : - string * argument_type list * (int * grammar_terminals) -> unit +val declare_extra_tactic_pprule : pp_tactic -> unit val exists_extra_tactic_pprule : string -> argument_type list -> bool |