From 846dad24f483bd5d5221a2b6fe663bbd5ba86455 Mon Sep 17 00:00:00 2001
From: Regis-Gianas <yrg@pps.univ-paris-diderot.fr>
Date: Thu, 30 Oct 2014 22:52:34 +0100
Subject: Ppvernacsig: New.   - Define the signature for a pretty-printer of
 vernacular commands.

Ppvernac: 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 28c57edba..01c835d89 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -8,3 +8,4 @@ Pptactic
 Printmod
 Prettyp
 Ppvernac
+Ppvernacsig
-- 
cgit v1.2.3