From fa6d5dd5efed2fe1f732d61eac126e39fef38305 Mon Sep 17 00:00:00 2001
From: Regis-Gianas <yrg@pps.univ-paris-diderot.fr>
Date: Tue, 4 Nov 2014 21:51:25 +0100
Subject: printing/Pptacticsig: New signature for tactic pretty-printers.
 printing/Pptactic: Use it.

---
 printing/printing.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/printing.mllib')

diff --git a/printing/printing.mllib b/printing/printing.mllib
index 713c2dee6..791070298 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -5,6 +5,7 @@ Ppconstr
 Ppconstrsig
 Printer
 Pptactic
+Pptacticsig
 Printmod
 Prettyp
 Ppvernac
-- 
cgit v1.2.3