diff options
Diffstat (limited to 'parsing/pptactic.mli')
| -rw-r--r-- | parsing/pptactic.mli | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index ca16c21e5..186a726f6 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -13,20 +13,24 @@ open Genarg open Tacexpr open Pretyping open Proof_type +open Topconstr +(* if the boolean is false then the extension applies only to old syntax *) val declare_extra_genarg_pprule : + bool -> ('a raw_abstract_argument_type * ('a -> std_ppcmds)) -> ('b closed_abstract_argument_type * ('b -> std_ppcmds)) -> unit +(* idem *) val declare_extra_tactic_pprule : - string -> + bool -> string -> (raw_generic_argument list -> string * Egrammar.grammar_tactic_production list) -> (closed_generic_argument list -> string * Egrammar.grammar_tactic_production list) -> unit -val pr_match_pattern : Tacexpr.pattern_expr match_pattern -> std_ppcmds +val pr_match_pattern : pattern_expr match_pattern -> std_ppcmds val pr_match_rule : bool -> (raw_tactic_expr -> std_ppcmds) -> (pattern_expr,raw_tactic_expr) match_rule -> std_ppcmds @@ -34,3 +38,18 @@ val pr_match_rule : bool -> (raw_tactic_expr -> std_ppcmds) -> val pr_raw_tactic : raw_tactic_expr -> std_ppcmds val pr_tactic : Proof_type.tactic_expr -> std_ppcmds + +val pr_rawgen: + (constr_expr -> std_ppcmds) -> + (raw_tactic_expr -> std_ppcmds) -> + (constr_expr, raw_tactic_expr) generic_argument -> + std_ppcmds +val pr_raw_extend: + (constr_expr -> std_ppcmds) -> + (raw_tactic_expr -> std_ppcmds) -> string -> + (constr_expr, raw_tactic_expr) generic_argument list -> + std_ppcmds +val pr_extend : + (raw_tactic_expr -> std_ppcmds) -> string -> + (Term.constr, raw_tactic_expr) generic_argument list -> + std_ppcmds |