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 | |
| 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')
| -rw-r--r-- | printing/richprinter.ml | 2 | ||||
| -rw-r--r-- | printing/richprinter.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/printing/richprinter.ml b/printing/richprinter.ml index a1c3305bb5..10ca118697 100644 --- a/printing/richprinter.ml +++ b/printing/richprinter.ml @@ -5,7 +5,7 @@ module RichppVernac = Ppvernac.Richpp module RichppTactic = Pptactic.Richpp type rich_pp = - (string, Ppannotation.t Richpp.located) Xml_datatype.gxml + (unit, Ppannotation.t Richpp.located) Xml_datatype.gxml * Xml_datatype.xml let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag 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. *) |