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 | |
| 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')
| -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 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 diff --git a/printing/richprinter.mli b/printing/richprinter.mli index 0621e606b6..41c313514b 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 ; *) - (unit, Ppannotation.t Richpp.located) Xml_datatype.gxml + Ppannotation.t Richpp.located Xml_datatype.gxml (** - an XML document, representing annotations as usual textual XML attributes. *) |