diff options
| author | Pierre-Marie Pédrot | 2016-09-15 13:33:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-15 13:34:18 +0200 |
| commit | 21dc493a93853525c5d9c33c0c7558909ce5e79d (patch) | |
| tree | 811b3c254c279f5e5b97003c05eac65c4ba76d7f /printing/printing.mllib | |
| parent | 404a8c619f76c572aec65f413baf087a374b37c3 (diff) | |
Moving Ltac printers to ltac/ folder.
Diffstat (limited to 'printing/printing.mllib')
| -rw-r--r-- | printing/printing.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/printing.mllib b/printing/printing.mllib index bc8f0750e1..b0141b6d37 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -3,7 +3,6 @@ Pputils Ppannotation Ppconstr Printer -Pptactic Printmod Prettyp Ppvernac |