From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- contrib/extraction/table.ml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) (limited to 'contrib/extraction/table.ml') diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index bd4fe924..b1a3cb31 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.ml 6555 2005-01-03 19:25:36Z sacerdot $ i*) +(*i $Id: table.ml 9310 2006-10-28 19:35:09Z herbelin $ i*) open Names open Term @@ -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 @@ -443,7 +441,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = Environ.constant_type env kn in + let typ = Typeops.type_of_constant env kn in let typ = Reduction.whd_betadeltaiota env typ in if Reduction.is_arity env typ then begin -- cgit v1.2.3