summaryrefslogtreecommitdiff
path: root/printing/richprinter.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
commit0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch)
tree12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /printing/richprinter.ml
parentcec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff)
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'printing/richprinter.ml')
-rw-r--r--printing/richprinter.ml7
1 files changed, 3 insertions, 4 deletions
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
index d71dc82d..d95e1907 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -5,21 +5,20 @@ module RichppVernac = Ppvernac.Richpp
module RichppTactic = Pptactic.Richpp
type rich_pp =
- string
- * 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
let make_richpp pr ast =
- let raw_pp, rich_pp =
+ let rich_pp =
rich_pp get_annotations (pr ast)
in
let xml = Ppannotation.(
xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
)
in
- (raw_pp, rich_pp, xml)
+ (rich_pp, xml)
let richpp_vernac = make_richpp RichppVernac.pr_vernac
let richpp_constr = make_richpp RichppConstr.pr_constr_expr