diff options
| author | Pierre-Marie Pédrot | 2015-08-15 19:27:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-08-15 20:05:40 +0200 |
| commit | 54fb2cdf7bb5c45f5a237b2559fd26d90d8f4df1 (patch) | |
| tree | 5b9f6879291476b13c81ae172b22836fe4c72f0c /printing/richprinter.mli | |
| parent | 98618cfb6b326b70da29348bc5d212e41086f473 (diff) | |
More invariants in Richpp.
We ensure statically by typing that the tags used by the rich printer
are integers. Furthermore, we also expose through typing that tags are
irrelevants in the returned XML.
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. *) |