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.ml | |
| 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.ml')
| -rw-r--r-- | printing/richprinter.ml | 2 |
1 files changed, 1 insertions, 1 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 |