diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 9173ab8cde..6e0e098c03 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -191,8 +191,6 @@ let judge_of_letin env name defj typj j = (* Type of an application. *) -let has_revert c = match kind_of_term c with Cast (c,REVERTcast,_) -> true | _ -> false - let judge_of_apply env funj argjv = let rec apply_rec n typ cst = function | [] -> @@ -203,8 +201,7 @@ let judge_of_apply env funj argjv = (match kind_of_term (whd_betadeltaiota env typ) with | Prod (_,c1,c2) -> (try - let l2r = has_revert hj.uj_val in - let c = conv_leq l2r env hj.uj_type c1 in + let c = conv_leq false env hj.uj_type c1 in let cst' = union_constraints cst c in apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl with NotConvertible -> @@ -268,12 +265,18 @@ let judge_of_product env name t1 t2 = let judge_of_cast env cj k tj = let expected_type = tj.utj_val in try - let cst = + let c, cst = match k with - | VMcast -> vm_conv CUMUL env cj.uj_type expected_type - | DEFAULTcast -> conv_leq false env cj.uj_type expected_type - | REVERTcast -> conv_leq true env cj.uj_type expected_type in - { uj_val = mkCast (cj.uj_val, k, expected_type); + | VMcast -> + mkCast (cj.uj_val, k, expected_type), + vm_conv CUMUL env cj.uj_type expected_type + | DEFAULTcast -> + mkCast (cj.uj_val, k, expected_type), + conv_leq false env cj.uj_type expected_type + | REVERTcast -> + cj.uj_val, + conv_leq true env cj.uj_type expected_type in + { uj_val = c; uj_type = expected_type }, cst with NotConvertible -> |