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 /lib/xml_parser.ml | |
| 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 'lib/xml_parser.ml')
0 files changed, 0 insertions, 0 deletions