diff options
Diffstat (limited to 'plugins/extraction/table.mli')
| -rw-r--r-- | plugins/extraction/table.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 7505664a60..978760e8e9 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -177,7 +177,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 -> unit +val print_extraction_inline : unit -> Pp.std_ppcmds val reset_extraction_inline : unit -> unit val extract_constant_inline : bool -> reference -> string list -> string -> unit |