diff options
Diffstat (limited to 'printing/pptactic.mli')
| -rw-r--r-- | printing/pptactic.mli | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 31346561..86e3ea54 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -11,11 +11,15 @@ open Pp open Genarg +open Geninterp open Names open Constrexpr open Tacexpr open Ppextend +type 'a grammar_tactic_prod_item_expr = +| TacTerm of string +| TacNonTerm of Loc.t * 'a * Names.Id.t type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> @@ -32,7 +36,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 +45,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 = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr 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 |