diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 114c5149f6..312c2eab3d 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -11,7 +11,6 @@ open Util open Names open Term open Vars -open Context open Declarations open Declareops open Environ @@ -26,6 +25,7 @@ open Globnames open Miniml open Table open Mlutil +open Context.Rel.Declaration (*i*) exception I of inductive_kind @@ -74,9 +74,9 @@ type flag = info * scheme Really important function. *) let rec flag_of_type env t : flag = - let t = whd_betadeltaiota env none t in + let t = whd_all env none t in match kind_of_term t with - | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c + | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) | Sort _ -> (Info,TypeScheme) | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default) @@ -102,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> (if is_info_scheme env t then Keep else Kill Kprop) :: (type_sign (push_rel_assum (n,t) env) d) | _ -> [] let rec type_scheme_nb_args env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in if is_info_scheme env t then n+1 else n @@ -135,7 +135,7 @@ let make_typvar n vl = next_ident_away id' vl let rec type_sign_vl env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in if not (is_info_scheme env t) then Kill Kprop::s, vl @@ -143,7 +143,7 @@ let rec type_sign_vl env c = | _ -> [],[] let rec nb_default_params env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let n = nb_default_params (push_rel_assum (n,t) env) d in if is_default env t then n+1 else n @@ -249,7 +249,7 @@ let rec extract_type env db j c args = | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop | Rel n -> (match lookup_rel n env with - | (_,Some t,_) -> extract_type env db j (lift n t) args + | LocalDef (_,t,_) -> extract_type env db j (lift n t) args | _ -> (* Asks [db] a translation for [n]. *) if n > List.length db then Tunknown @@ -489,7 +489,7 @@ and extract_really_ind env kn mib = *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let env' = push_rel_assum (n,t) env in let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in @@ -573,7 +573,7 @@ let rec extract_term env mle mlt c args = put_magic_if magic (MLlam (id, d'))) | LetIn (n, c1, t1, c2) -> let id = id_of_name n in - let env' = push_rel (Name id, Some c1, t1) env in + let env' = push_rel (LocalDef (Name id, c1, t1)) env in (* We directly push the args inside the [LetIn]. TODO: the opt_let_app flag is supposed to prevent that *) let args' = List.map (lift 1) args in @@ -684,7 +684,7 @@ and extract_cst_app env mle mlt kn u args = let l,l' = List.chop (projection_arity (ConstRef kn)) mla in if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l' else mla - with e when Errors.noncritical e -> mla + with e when CErrors.noncritical e -> mla in (* For strict languages, purely logical signatures lead to a dummy lam (except when [Kill Ktype] everywhere). So a [MLdummy] is left @@ -848,7 +848,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = let decomp_lams_eta_n n m env c t = let rels = fst (splay_prod_n env none n t) in - let rels = List.map (fun (id,_,c) -> (id,c)) rels in + let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in let rels',c = decompose_lam c in let d = n - m in (* we'd better keep rels' as long as possible. *) |