diff options
| author | notin | 2006-10-04 13:41:33 +0000 |
|---|---|---|
| committer | notin | 2006-10-04 13:41:33 +0000 |
| commit | c7545949a5f4c229aac731e482c3bdc769863f41 (patch) | |
| tree | 1a67d15ff89d9aceef597acdda7a8a53ad086de2 | |
| parent | 79fba16cf02b83ac2b4866e582dd4481314770b4 (diff) | |
Correction bug #1211
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9205 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |