From 98618cfb6b326b70da29348bc5d212e41086f473 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 15 Aug 2015 19:17:26 +0200
Subject: More parametric type for generalized XML.

---
 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 d95e190749..a1c3305bb5 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -5,7 +5,7 @@ module RichppVernac = Ppvernac.Richpp
 module RichppTactic = Pptactic.Richpp
 
 type rich_pp =
-    Ppannotation.t Richpp.located Xml_datatype.gxml
+    (string, 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 41c313514b..3875e17237 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 ; *)
-    Ppannotation.t Richpp.located Xml_datatype.gxml
+    (string, Ppannotation.t Richpp.located) Xml_datatype.gxml
 
     (** - an XML document, representing annotations as usual textual
         XML attributes. *)
-- 
cgit v1.2.3