summaryrefslogtreecommitdiff
path: root/contrib/extraction
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /contrib/extraction
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/extract_env.ml5
-rw-r--r--contrib/extraction/extraction.ml19
-rw-r--r--contrib/extraction/table.ml18
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