diff options
| author | Pierre-Marie Pédrot | 2015-08-15 19:17:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-08-15 20:05:34 +0200 |
| commit | 98618cfb6b326b70da29348bc5d212e41086f473 (patch) | |
| tree | b47e7955c5c35f1c415c68fd6a2e97b5745fc32a /printing | |
| parent | 2c1882815e7877bfc574f9f71eff6ce099145df5 (diff) | |
More parametric type for generalized XML.
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 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. *) |