From 76992bd0bab4d5b59e19d7a6a21c091f1c5d8340 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 25 Apr 2016 12:34:34 +0200
Subject: Removing dead code related to printing of ML tactics in Pptactic.

---
 printing/pptactic.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'printing/pptactic.mli')

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
-- 
cgit v1.2.3