aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evardefine.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evardefine.ml')
-rw-r--r--pretyping/evardefine.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index d349cf821..f9ab75cea 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -78,7 +78,7 @@ let define_pure_evar_as_product evd evk =
let evi = Evd.find_undefined evd evk in
let evenv = evar_env evi in
let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
- let concl = Reductionops.whd_betadeltaiota evenv evd evi.evar_concl in
+ let concl = Reductionops.whd_all evenv evd evi.evar_concl in
let s = destSort concl in
let evd1,(dom,u1) =
let evd = Sigma.Unsafe.of_evar_map evd in
@@ -131,7 +131,7 @@ let define_pure_evar_as_lambda env evd evk =
let open Context.Named.Declaration in
let evi = Evd.find_undefined evd evk in
let evenv = evar_env evi in
- let typ = Reductionops.whd_betadeltaiota evenv evd (evar_concl evi) in
+ let typ = Reductionops.whd_all evenv evd (evar_concl evi) in
let evd1,(na,dom,rng) = match kind_of_term typ with
| Prod (na,dom,rng) -> (evd,(na,dom,rng))
| Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
@@ -169,7 +169,7 @@ let define_evar_as_sort env evd (ev,args) =
let evd, u = new_univ_variable univ_rigid evd in
let evi = Evd.find_undefined evd ev in
let s = Type u in
- let concl = Reductionops.whd_betadeltaiota (evar_env evi) evd evi.evar_concl in
+ let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in
let sort = destSort concl in
let evd' = Evd.define ev (mkSort s) evd in
Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
@@ -181,10 +181,10 @@ let define_evar_as_sort env evd (ev,args) =
let split_tycon loc env evd tycon =
let rec real_split evd c =
- let t = Reductionops.whd_betadeltaiota env evd c in
+ let t = Reductionops.whd_all env evd c in
match kind_of_term t with
| Prod (na,dom,rng) -> evd, (na, dom, rng)
- | Evar ev (* ev is undefined because of whd_betadeltaiota *) ->
+ | Evar ev (* ev is undefined because of whd_all *) ->
let (evd',prod) = define_evar_as_product evd ev in
let (_,dom,rng) = destProd prod in
evd',(Anonymous, dom, rng)