From e3c247c1d96f39d2c07d120b69598a904b7d9f19 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Sun, 11 Jun 2017 15:14:15 +0200 Subject: deprecate Pp.std_ppcmds type alias --- plugins/extraction/table.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 2b3007f02..7e47d0bc8 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -191,7 +191,7 @@ val find_custom_match : ml_branch array -> string val extraction_language : lang -> unit val extraction_inline : bool -> reference list -> unit -val print_extraction_inline : unit -> Pp.std_ppcmds +val print_extraction_inline : unit -> Pp.t val reset_extraction_inline : unit -> unit val extract_constant_inline : bool -> reference -> string list -> string -> unit @@ -206,7 +206,7 @@ val extraction_implicit : reference -> int_or_id list -> unit val extraction_blacklist : Id.t list -> unit val reset_extraction_blacklist : unit -> unit -val print_extraction_blacklist : unit -> Pp.std_ppcmds +val print_extraction_blacklist : unit -> Pp.t -- cgit v1.2.3