diff options
Diffstat (limited to 'printing/ppvernac.mli')
| -rw-r--r-- | printing/ppvernac.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index ed5585b30..b88eed484 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -10,10 +10,10 @@ objects and their subcomponents. *) (** Prints a fixpoint body *) -val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds +val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t (** Prints a vernac expression *) -val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds +val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t (** Prints a vernac expression and closes it with a dot. *) -val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds +val pr_vernac : Vernacexpr.vernac_expr -> Pp.t |