diff options
| author |  Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 13:29:32 +0100 |
|---|---|---|
| committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:36 +0100 |
| commit | 7b3f2d2783f74a38b4fe40d2dc5f58b8d5bae0f1 (patch) | |
| tree | 09da2824783d0b3872e21c045b104f12712a0985 /printing | |
| parent | 6905915f7ce8989dc64473118ada94adf9a20cd9 (diff) | |
printing/richPrinter: Fix incorrect signatures.
Diffstat (limited to 'printing')
| -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 5249691e1..07e97668c 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 2f97cc3fe..60d002596 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 |