diff options
| author | Pierre-Marie Pédrot | 2015-01-21 10:55:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-23 21:30:43 +0100 |
| commit | 43c6f29edde078726f10144c0d241a882ebdd13d (patch) | |
| tree | 822e23aa496c5d3284709c060bb56073536cc362 /printing/pptactic.mli | |
| parent | 87106cd6a0e613fc61943959d8fc7d3ff025fc5d (diff) | |
Splitting ML tactics in one function per grammar entry.
Furthermore, ML tactic dispatch is not done according to the
type of its argument anymore.
Diffstat (limited to 'printing/pptactic.mli')
| -rw-r--r-- | printing/pptactic.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 284237f014..50cc4e2bc2 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -50,7 +50,7 @@ type pp_tactic = { pptac_prods : int * grammar_terminals; } -val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit +val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit (** The default pretty-printers produce {!Pp.std_ppcmds} that are |