diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 12 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 4 |
2 files changed, 8 insertions, 8 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0153348de..4308b4633 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_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 (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_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 @@ -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 diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 81dfa603d..3a9ecc9ff 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -441,7 +441,7 @@ let error_MPfile_as_mod mp b = let argnames_of_global r = let typ = Global.type_of_global_unsafe r in let rels,_ = - decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in + decompose_prod (Reduction.whd_all (Global.env ()) typ) in List.rev_map fst rels let msg_of_implicit = function @@ -880,7 +880,7 @@ let extract_constant_inline inline r ids s = | ConstRef kn -> let env = Global.env () in let typ = Global.type_of_global_unsafe (ConstRef kn) in - let typ = Reduction.whd_betadeltaiota env typ in + let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin let nargs = Hook.get use_type_scheme_nb_args env typ in |