diff options
| author | Pierre-Marie Pédrot | 2015-08-15 21:49:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-08-15 21:51:36 +0200 |
| commit | 2f5bc3148579ff359f179c758a7f4e724a14adf7 (patch) | |
| tree | 36dd8a606a44d84bb5f081c518693a02efc6df67 /printing/richprinter.ml | |
| 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.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 |