diff options
| -rw-r--r-- | contrib/extraction/table.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index ce2a99c6d7..596f3ccb0b 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -140,16 +140,14 @@ let error_axiom_scheme r i = str " type variable(s).") let warning_info_ax r = - Options.if_verbose msg_warning - (str "You must realize axiom " ++ - pr_global r ++ str " in the extracted code.") + msg_warning (str "You must realize axiom " ++ + pr_global r ++ str " in the extracted code.") let warning_log_ax r = - Options.if_verbose msg_warning - (str "This extraction depends on logical axiom" ++ spc () ++ - pr_global r ++ str "." ++ spc() ++ - str "Having false logical axiom in the environment when extracting" ++ - spc () ++ str "may lead to incorrect or non-terminating ML terms.") + msg_warning (str "This extraction depends on logical axiom" ++ spc () ++ + pr_global r ++ str "." ++ spc() ++ + str "Having false logical axiom in the environment when extracting" ++ + spc () ++ str "may lead to incorrect or non-terminating ML terms.") let check_inside_module () = try |