diff options
Diffstat (limited to 'printing/pptactic.mli')
| -rw-r--r-- | printing/pptactic.mli | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 313465614..1608cae75 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -32,7 +32,7 @@ type 'a glob_extra_genarg_printer = type 'a extra_genarg_printer = (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (tolerability -> Val.t -> std_ppcmds) -> 'a -> std_ppcmds val declare_extra_genarg_pprule : @@ -41,14 +41,13 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit -type grammar_terminals = string option list +type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list type pp_tactic = { - pptac_args : argument_type list; - pptac_prods : int * grammar_terminals; + pptac_level : int; + pptac_prods : grammar_terminals; } -val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit (** The default pretty-printers produce {!Pp.std_ppcmds} that are |