From 8df8bc8e3e2aa67f02a83db02fbbe877fa0b0450 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 6 Jun 2016 18:15:42 +0200 Subject: printing.mllib: remove some other .mli-only from a .mllib --- printing/printing.mllib | 3 --- 1 file changed, 3 deletions(-) (limited to 'printing/printing.mllib') diff --git a/printing/printing.mllib b/printing/printing.mllib index 52102e1d3..bc8f0750e 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -2,11 +2,8 @@ Genprint Pputils Ppannotation Ppconstr -Ppconstrsig Printer Pptactic -Pptacticsig Printmod Prettyp Ppvernac -Ppvernacsig -- cgit v1.2.3