From 2f5bc3148579ff359f179c758a7f4e724a14adf7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 15 Aug 2015 21:49:22 +0200
Subject: 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.
---
 printing/richprinter.ml  | 2 +-
 printing/richprinter.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing')

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. *)
-- 
cgit v1.2.3