diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-06 18:15:42 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-07 16:12:02 +0200 |
| commit | 8df8bc8e3e2aa67f02a83db02fbbe877fa0b0450 (patch) | |
| tree | 0e516a32ae7c871d7fa4dda8cb9a75b9205e1ad6 /printing/printing.mllib | |
| parent | a0970a6bef365a31ae780f2b7d673f5f4ae37aa9 (diff) | |
printing.mllib: remove some other .mli-only from a .mllib
Diffstat (limited to 'printing/printing.mllib')
| -rw-r--r-- | printing/printing.mllib | 3 |
1 files changed, 0 insertions, 3 deletions
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 |