diff options
Diffstat (limited to 'printing/ppvernac.mli')
| -rw-r--r-- | printing/ppvernac.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index 5e0cc8da5..603be6308 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -9,7 +9,7 @@ (** 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 +val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t (** Prints a fixpoint body *) val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t |