diff options
Diffstat (limited to 'plugins/extraction/table.mli')
| -rw-r--r-- | plugins/extraction/table.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 |