diff options
Diffstat (limited to 'printing/richPrinter.mli')
| -rw-r--r-- | printing/richPrinter.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |