diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
-rw-r--r-- | plugins/extraction/extraction.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 85cacecdb..6ca34036a 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -74,7 +74,7 @@ type flag = info * scheme Really important function. *) let rec flag_of_type env t : flag = - let t = whd_all env none t in + let t = whd_all env none (EConstr.of_constr t) in match kind_of_term t with | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) @@ -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_all env none c) with + match kind_of_term (whd_all env none (EConstr.of_constr 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_all env none c) with + match kind_of_term (whd_all env none (EConstr.of_constr 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_all env none c) with + match kind_of_term (whd_all env none (EConstr.of_constr 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_all env none c) with + match kind_of_term (whd_all env none (EConstr.of_constr 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 @@ -214,7 +214,7 @@ let parse_ind_args si args relmax = let rec extract_type env db j c args = - match kind_of_term (whd_betaiotazeta Evd.empty c) with + match kind_of_term (whd_betaiotazeta none (EConstr.of_constr c)) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env db j d (Array.to_list args' @ args) @@ -297,7 +297,7 @@ and extract_type_app env db (r,s) args = let ml_args = List.fold_right (fun (b,c) a -> if b == Keep then - let p = List.length (fst (splay_prod env none (type_of env c))) in + let p = List.length (fst (splay_prod env none (EConstr.of_constr (type_of env c)))) in let db = iterate (fun l -> 0 :: l) p db in (extract_type_scheme env db c p) :: a else a) @@ -316,12 +316,12 @@ and extract_type_app env db (r,s) args = and extract_type_scheme env db c p = if Int.equal p 0 then extract_type env db 0 c [] else - let c = whd_betaiotazeta Evd.empty c in + let c = whd_betaiotazeta none (EConstr.of_constr c) in match kind_of_term c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) | _ -> - let rels = fst (splay_prod env none (type_of env c)) in + let rels = fst (splay_prod env none (EConstr.of_constr (type_of env c))) in let env = push_rels_assum rels env in let eta_args = List.rev_map mkRel (List.interval 1 p) in extract_type env db 0 (lift p c) eta_args @@ -488,7 +488,7 @@ and extract_really_ind env kn mib = *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_all env none c) with + match kind_of_term (whd_all env none (EConstr.of_constr 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 @@ -846,7 +846,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *) let decomp_lams_eta_n n m env c t = - let rels = fst (splay_prod_n env none n t) in + let rels = fst (splay_prod_n env none n (EConstr.of_constr t)) 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 |