diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-15 21:49:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-15 21:51:36 +0200 |
| commit | 2f5bc3148579ff359f179c758a7f4e724a14adf7 (patch) | |
| tree | 36dd8a606a44d84bb5f081c518693a02efc6df67 /printing/richprinter.mli | |
| parent | 54fb2cdf7bb5c45f5a237b2559fd26d90d8f4df1 (diff) | |
Revert the four previous commits and update the description of Richpp.
Correcting the code w.r.t. to the API was not the right solution. Instead,
the API comment had to be corrected.
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 0621e606b..41c313514 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 ; *) - (unit, Ppannotation.t Richpp.located) Xml_datatype.gxml + Ppannotation.t Richpp.located Xml_datatype.gxml (** - an XML document, representing annotations as usual textual XML attributes. *) |