Imported Upstream version 8.1~gammaupstream/8.1.gamma

3 files changed, 21 insertions, 21 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index c581c620..2d425e9f 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.ml 6328 2004-11-18 17:31:41Z sacerdot $ i*)
+(*i $Id: extract_env.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
 
 open Term
 open Declarations
@@ -74,7 +74,8 @@ let visit_ref v r =
 exception Impossible
 
 let check_arity env cb = 
-  if Reduction.is_arity env cb.const_type then raise Impossible
+  let t = Typeops.type_of_constant_type env cb.const_type in
+  if Reduction.is_arity env t then raise Impossible
 
 let check_fix env cb i = 
   match cb.const_body with 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 2b4b7967..52e7f1dd 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml 9032 2006-07-07 16:30:34Z herbelin $ i*)
+(*i $Id: extraction.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -225,7 +225,7 @@ let rec extract_type env db j c args =
     | Const kn -> 
 	let r = ConstRef kn in 
 	let cb = lookup_constant kn env in 
-	let typ = cb.const_type in 
+	let typ = Typeops.type_of_constant_type env cb.const_type in 
 	(match flag_of_type env typ with 
 	   | (Info, TypeScheme) -> 
 	       let mlt = extract_type_app env db (r, type_sign env typ) args in 
@@ -321,7 +321,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
       Array.map 
 	(fun mip ->
 	   let b = snd (mind_arity mip) <> InProp in
-	   let ar = Inductive.type_of_inductive (mib,mip) in
+	   let ar = Inductive.type_of_inductive env (mib,mip) in
 	   let s,v = if b then type_sign_vl env ar else [],[] in
 	   let t = Array.make (Array.length mip.mind_nf_lc) [] in 
 	   { ip_typename = mip.mind_typename;
@@ -401,7 +401,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	(* Is this record officially declared with its projections ? *)
 	(* If so, we use this information. *)
 	begin try 
-	  let n = nb_default_params env (Inductive.type_of_inductive(mib,mip0))
+	  let n = nb_default_params env
+            (Inductive.type_of_inductive env (mib,mip0))
 	  in
 	  List.iter 
 	    (option_iter 
@@ -446,7 +447,7 @@ and mlt_env env r = match r with
 	   | _ -> None
        with Not_found -> 
 	 let cb = Environ.lookup_constant kn env in
-	 let typ = cb.const_type in
+	 let typ = Typeops.type_of_constant_type env cb.const_type in 
 	 match cb.const_body with
 	   | None -> None
 	   | Some l_body -> 
@@ -473,7 +474,7 @@ let record_constant_type env kn opt_typ =
     lookup_type kn 
   with Not_found ->
     let typ = match opt_typ with 
-      | None -> constant_type env kn 
+      | None -> Typeops.type_of_constant env kn
       | Some typ -> typ 
     in let mlt = extract_type env [] 1 typ [] 
     in let schema = (type_maxvar mlt, mlt)
@@ -814,7 +815,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 		 
 let extract_constant env kn cb = 
   let r = ConstRef kn in 
-  let typ = cb.const_type in
+  let typ = Typeops.type_of_constant_type env cb.const_type in 
   match cb.const_body with
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
@@ -846,7 +847,7 @@ let extract_constant env kn cb =
 
 let extract_constant_spec env kn cb = 
   let r = ConstRef kn in 
-  let typ = cb.const_type in
+  let typ = Typeops.type_of_constant_type env cb.const_type in 
   match flag_of_type env typ with 
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
     | (Logic, Default) -> Sval (r, Tdummy Kother) 
@@ -884,7 +885,7 @@ let extract_declaration env r = match r with
 type kind = Logical | Term | Type 
     
 let constant_kind env cb = 
-  match flag_of_type env cb.const_type with 
+  match flag_of_type env (Typeops.type_of_constant_type env cb.const_type) with 
     | (Logic,_) -> Logical
     | (Info,TypeScheme) -> Type
     | (Info,Default) -> Term
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