diff options
Diffstat (limited to 'printing/richprinter.mli')
| -rw-r--r-- | printing/richprinter.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/richprinter.mli b/printing/richprinter.mli index 3875e17237..0621e606b6 100644 --- a/printing/richprinter.mli +++ b/printing/richprinter.mli @@ -23,7 +23,7 @@ type rich_pp = (** - a generalized semi-structured document whose attributes are annotations ; *) - (string, Ppannotation.t Richpp.located) Xml_datatype.gxml + (unit, Ppannotation.t Richpp.located) Xml_datatype.gxml (** - an XML document, representing annotations as usual textual XML attributes. *) |