diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2print.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/tac2print.mli b/src/tac2print.mli index ddd599641d..2ee5cf42e0 100644 --- a/src/tac2print.mli +++ b/src/tac2print.mli @@ -19,16 +19,16 @@ type typ_level = | T1 | T0 -val pr_typref : type_constant -> std_ppcmds -val pr_glbtype_gen : ('a -> string) -> typ_level -> 'a glb_typexpr -> std_ppcmds -val pr_glbtype : ('a -> string) -> 'a glb_typexpr -> std_ppcmds +val pr_typref : type_constant -> Pp.t +val pr_glbtype_gen : ('a -> string) -> typ_level -> 'a glb_typexpr -> Pp.t +val pr_glbtype : ('a -> string) -> 'a glb_typexpr -> Pp.t (** {5 Printing expressions} *) -val pr_constructor : ltac_constructor -> std_ppcmds -val pr_projection : ltac_projection -> std_ppcmds -val pr_glbexpr_gen : exp_level -> glb_tacexpr -> std_ppcmds -val pr_glbexpr : glb_tacexpr -> std_ppcmds +val pr_constructor : ltac_constructor -> Pp.t +val pr_projection : ltac_projection -> Pp.t +val pr_glbexpr_gen : exp_level -> glb_tacexpr -> Pp.t +val pr_glbexpr : glb_tacexpr -> Pp.t (** {5 Utilities} *) |