diff options
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 10ca118697..d95e190749 100644 --- a/printing/richprinter.ml +++ b/printing/richprinter.ml @@ -5,7 +5,7 @@ module RichppVernac = Ppvernac.Richpp module RichppTactic = Pptactic.Richpp type rich_pp = - (unit, Ppannotation.t Richpp.located) Xml_datatype.gxml + Ppannotation.t Richpp.located Xml_datatype.gxml * Xml_datatype.xml let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag |