diff options
Diffstat (limited to 'printing/richPrinter.ml')
| -rw-r--r-- | printing/richPrinter.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/printing/richPrinter.ml b/printing/richPrinter.ml index 5249691e1f..07e97668c6 100644 --- a/printing/richPrinter.ml +++ b/printing/richPrinter.ml @@ -5,6 +5,11 @@ module Indexer = Indexer (struct type t = Ppannotation.t end) module RichPpConstr = Ppconstr.RichPp (Indexer) module RichPpVernac = Ppvernac.RichPp (Indexer) +type rich_pp = + string + * Ppannotation.t RichPp.located Xml_datatype.gxml + * Xml_datatype.xml + let richpp_vernac phrase_ast = let raw_pp, rich_pp = rich_pp Indexer.get_annotations (fun () -> RichPpVernac.pr_vernac phrase_ast) |