aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-03-28 10:17:11 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-03-28 10:17:11 +0000
commit64354facef5a7d57df538e416d6c3564e3157a98 (patch)
tree390a7a88bc5e027e61081c7faa61d83675adc48f
parente59c5cf5c19084e49cb4817c8950c8ce90324fcc (diff)
petite erreur dans le typage des let-in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2573 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--kernel/typeops.ml20
-rw-r--r--kernel/typeops.mli2
-rw-r--r--pretyping/typing.ml4
3 files changed, 13 insertions, 13 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 9d63dc7dd..4606734fe 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -156,9 +156,8 @@ let judge_of_abstraction env name var j =
(* Type of let-in. *)
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
+ uj_type = type_app (subst1 defj.uj_val) j.uj_type }
(* Type of an application. *)
@@ -229,13 +228,14 @@ let judge_of_product env name t1 t2 =
*)
let judge_of_cast env cj tj =
+ let expected_type = tj.utj_val in
try
- let cst = conv_leq env cj.uj_type tj.utj_val in
- { uj_val = mkCast (j_val cj, tj.utj_val);
- uj_type = tj.utj_val },
+ let cst = conv_leq env cj.uj_type expected_type in
+ { uj_val = mkCast (j_val cj, expected_type);
+ uj_type = expected_type },
cst
with NotConvertible ->
- error_actual_type env cj tj.utj_val
+ error_actual_type env cj expected_type
(* Inductive types. *)
@@ -367,11 +367,11 @@ let rec execute env cstr cu =
| LetIn (name,c1,c2,c3) ->
let (j1,cu1) = execute env c1 cu in
- let (j2,cu2) = execute_type env c2 cu in
+ let (j2,cu2) = execute_type env c2 cu1 in
+ let (_,cu3) = univ_combinator cu2 (judge_of_cast env j1 j2) in
let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
- let (j',cu2) = execute env1 c3 cu1 in
- univ_combinator cu2
- (judge_of_letin env name j1 j2 j')
+ let (j',cu4) = execute env1 c3 cu3 in
+ (judge_of_letin env name j1 j2 j', cu4)
| Cast (c,t) ->
let (cj,cu1) = execute env c cu in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 2a678cd49..6980c9759 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -68,7 +68,7 @@ val judge_of_product :
(* s Type of a let in. *)
val judge_of_letin :
env -> name -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment
- -> unsafe_judgment * constraints
+ -> unsafe_judgment
(*s Type of a cast. *)
val judge_of_cast :
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 9a6008832..f84cdc632 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -113,10 +113,10 @@ let rec execute mf env sigma cstr =
let j1 = execute mf env sigma c1 in
let j2 = execute mf env sigma c2 in
let j2 = type_judgment env sigma j2 in
+ let _ = conv_leq env sigma j1.uj_type j2.utj_val in
let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
let j3 = execute mf env1 sigma c3 in
- let (j,_) = judge_of_letin env name j1 j2 j3 in
- j
+ judge_of_letin env name j1 j2 j3
| Cast (c,t) ->
let cj = execute mf env sigma c in