diff options
Diffstat (limited to 'kernel/fast_typeops.ml')
| -rw-r--r-- | kernel/fast_typeops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index c2c8ee242..e28d770e8 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -35,12 +35,12 @@ let check_constraints cst env = (* This should be a type (a priori without intention to be an assumption) *) let type_judgment env c t = - match kind_of_term(whd_betadeltaiota env t) with + match kind_of_term(whd_all env t) with | Sort s -> {utj_val = c; utj_type = s } | _ -> error_not_type env (make_judge c t) let check_type env c t = - match kind_of_term(whd_betadeltaiota env t) with + match kind_of_term(whd_all env t) with | Sort s -> s | _ -> error_not_type env (make_judge c t) @@ -157,7 +157,7 @@ let judge_of_apply env func funt argsv argstv = let rec apply_rec i typ = if Int.equal i len then typ else - (match kind_of_term (whd_betadeltaiota env typ) with + (match kind_of_term (whd_all env typ) with | Prod (_,c1,c2) -> let arg = argsv.(i) and argt = argstv.(i) in (try |