diff options
| author | Pierre-Marie Pédrot | 2016-04-25 12:34:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-25 12:35:27 +0200 |
| commit | 76992bd0bab4d5b59e19d7a6a21c091f1c5d8340 (patch) | |
| tree | de075b506538c43a66f199f1403ea0a67536d0c1 /printing/pptactic.mli | |
| parent | a7917a32b24b652d2978a7aea171aa01da37eece (diff) | |
Removing dead code related to printing of ML tactics in Pptactic.
Diffstat (limited to 'printing/pptactic.mli')
| -rw-r--r-- | printing/pptactic.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 31a5a5d4a8..1608cae751 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -48,7 +48,6 @@ type pp_tactic = { pptac_prods : grammar_terminals; } -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 |