diff options
| -rw-r--r-- | printing/richPrinter.ml | 5 | ||||
| -rw-r--r-- | printing/richPrinter.mli | 2 |
2 files changed, 6 insertions, 1 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) diff --git a/printing/richPrinter.mli b/printing/richPrinter.mli index 2f97cc3fe2..60d002596a 100644 --- a/printing/richPrinter.mli +++ b/printing/richPrinter.mli @@ -32,4 +32,4 @@ type rich_pp = * Xml_datatype.xml (** [richpp_vernac phrase] produces a rich pretty-printing of [phrase]. *) -val richpp_vernac : Vernac.vernac_expr -> rich_pp +val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp |