diff options
| author | Pierre-Marie Pédrot | 2017-08-02 12:15:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 12:15:05 +0200 |
| commit | d0766f4dc08b00128a47a00ca74334ba0bfeed24 (patch) | |
| tree | cacc7a3a67cadccb6d62298dcb193a8d1c5af629 /src | |
| parent | 53374f189cc9b9b67ff94d5362fdffdba6c779a3 (diff) | |
Removing deprecated stuff.
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} *) |