diff options
| author | Regis-Gianas | 2014-10-30 22:31:27 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:35 +0100 |
| commit | 2656c62e9be7a856f12c0da0740869d193273c4d (patch) | |
| tree | 96792a9ccb608e795857f784bc6373eebfd4635c /printing/printing.mllib | |
| parent | 0aa24d51d2606549da87ed42085f612f2dbb1428 (diff) | |
Ppannotation: New.
Define the annotations stored in semi-structured pretty-prints.
Ppconstrsig: New.
Contains the signature of a pretty-printer for ppconstr.
Ppconstr: Export a new rich pretty-printer for constr_expr and co.
Diffstat (limited to 'printing/printing.mllib')
| -rw-r--r-- | printing/printing.mllib | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/printing.mllib b/printing/printing.mllib index 2a8f1030fe..28c57edba0 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,6 +1,8 @@ Genprint Pputils +Ppannotation Ppconstr +Ppconstrsig Printer Pptactic Printmod |