diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 0efdbbb6b5..62ce89896a 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -430,8 +430,8 @@ let check_loaded_modfile mp = match base_mp mp with | _ -> () let info_file f = - Flags.if_verbose message - ("The file "^f^" has been created by extraction.") + Flags.if_verbose msg_info + (str ("The file "^f^" has been created by extraction.")) (*S The Extraction auxiliary commands *) @@ -738,8 +738,7 @@ let extraction_blacklist l = (* Printing part *) let print_extraction_blacklist () = - msgnl - (prlist_with_sep fnl pr_id (Idset.elements !blacklist_table)) + prlist_with_sep fnl pr_id (Idset.elements !blacklist_table) (* Reset part *) |