diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pptactic.ml | 2 | ||||
| -rw-r--r-- | parsing/pptactic.mli | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3f02cf309e..d5c42a04d7 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -42,6 +42,8 @@ let declare_extra_tactic_pprule for_v8 s (tags,prods) = Hashtbl.add prtac_tab_v7 (s,tags) prods; if for_v8 then Hashtbl.add prtac_tab (s,tags) prods +let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab_v7 (s,tags) + type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 9e1555ce91..bd42a1ffeb 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -53,6 +53,8 @@ type grammar_terminals = string option list val declare_extra_tactic_pprule : bool -> string -> argument_type list * (int * grammar_terminals) -> unit +val exists_extra_tactic_pprule : string -> argument_type list -> bool + val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> |