diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-08 14:10:21 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-08 14:10:21 +0000 |
commit | 25ea09274a8b085092963fcccf0400f8826f5544 (patch) | |
tree | 3cddd41152c9efec8baccf65553164ab8cae8513 /kernel/typeops.ml | |
parent | 8640627fa00798b429baf56937a66f1621be0a02 (diff) |
Rétablissement de la persistance des Cast; typage des LetIn sans recours à Cast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2171 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
-rw-r--r-- | kernel/typeops.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index a2c6fe686..e99673fe1 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -156,12 +156,10 @@ let judge_of_abstraction env name var j = (* Type of let-in. *) -let judge_of_letin env name defj j = - let v = match kind_of_term defj.uj_val with - Cast(c,t) -> c - | _ -> defj.uj_val in - { uj_val = mkLetIn (name, v, defj.uj_type, j.uj_val) ; - uj_type = type_app (subst1 v) j.uj_type } +let judge_of_letin env name defj typj j = + let cst = conv_leq env defj.uj_type typj.utj_val in + { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; + uj_type = type_app (subst1 defj.uj_val) j.uj_type }, cst (* Type of an application. *) @@ -237,7 +235,7 @@ let judge_of_product env name t1 t2 = let judge_of_cast env cj tj = try let cst = conv_leq env cj.uj_type tj.utj_val in - { uj_val = j_val cj; + { uj_val = mkCast (j_val cj, tj.utj_val); uj_type = tj.utj_val }, cst with NotConvertible -> @@ -373,10 +371,12 @@ let rec execute env cstr cu = (judge_of_product env name varj varj') | LetIn (name,c1,c2,c3) -> - let (j,cu1) = execute env (mkCast(c1,c2)) cu in - let env1 = push_rel (name,Some j.uj_val,j.uj_type) env in + let (j1,cu1) = execute env c1 cu in + let (j2,cu2) = execute_type env c2 cu in + let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in let (j',cu2) = execute env1 c3 cu1 in - (judge_of_letin env name j j', cu2) + univ_combinator cu2 + (judge_of_letin env name j1 j2 j') | Cast (c,t) -> let (cj,cu1) = execute env c cu in |