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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/richprinter.ml')

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