From 54fb2cdf7bb5c45f5a237b2559fd26d90d8f4df1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 15 Aug 2015 19:27:43 +0200
Subject: More invariants in Richpp.

We ensure statically by typing that the tags used by the rich printer
are integers. Furthermore, we also expose through typing that tags are
irrelevants in the returned XML.
---
 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 a1c3305bb5..10ca118697 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -5,7 +5,7 @@ module RichppVernac = Ppvernac.Richpp
 module RichppTactic = Pptactic.Richpp
 
 type rich_pp =
-    (string, Ppannotation.t Richpp.located) Xml_datatype.gxml
+    (unit, Ppannotation.t Richpp.located) Xml_datatype.gxml
     * Xml_datatype.xml
 
 let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
-- 
cgit v1.2.3