diff options
Diffstat (limited to 'printing/richprinter.mli')
| -rw-r--r-- | printing/richprinter.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/printing/richprinter.mli b/printing/richprinter.mli index c67d52c0..41c31351 100644 --- a/printing/richprinter.mli +++ b/printing/richprinter.mli @@ -20,12 +20,10 @@ (** A rich pretty-print is composed of: *) type rich_pp = - (** - a raw pretty-print ; *) - string (** - a generalized semi-structured document whose attributes are annotations ; *) - * Ppannotation.t Richpp.located Xml_datatype.gxml + Ppannotation.t Richpp.located Xml_datatype.gxml (** - an XML document, representing annotations as usual textual XML attributes. *) |