diff options
Diffstat (limited to 'printing/ppvernac.mli')
| -rw-r--r-- | printing/ppvernac.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index 34b4fb97f..5e0cc8da5 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -9,6 +9,8 @@ (** This module implements pretty-printers for vernac_expr syntactic objects and their subcomponents. *) +val pr_set_entry_type : ('a,'b) Extend.constr_entry_key_gen -> Pp.t + (** Prints a fixpoint body *) val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t |