diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.ml | 2 | ||||
| -rw-r--r-- | kernel/typeops.ml | 21 |
2 files changed, 14 insertions, 9 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index b308b22a4b..b4ddbfc8c7 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -562,6 +562,8 @@ let compare_constr f t1 t2 = | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2 + | App (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2 + | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2)) | App (c1,l1), App (c2,l2) -> Array.length l1 = Array.length l2 && f c1 c2 && array_for_all2 f l1 l2 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 -> |