From c7545949a5f4c229aac731e482c3bdc769863f41 Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 4 Oct 2006 13:41:33 +0000
Subject: Correction bug #1211

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9205 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/table.ml | 14 ++++++--------
 1 file 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 
-- 
cgit v1.2.3