diff options
author | 2002-03-28 10:17:11 +0000 | |
---|---|---|
committer | 2002-03-28 10:17:11 +0000 | |
commit | 64354facef5a7d57df538e416d6c3564e3157a98 (patch) | |
tree | 390a7a88bc5e027e61081c7faa61d83675adc48f /pretyping/typing.ml | |
parent | e59c5cf5c19084e49cb4817c8950c8ce90324fcc (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
Diffstat (limited to 'pretyping/typing.ml')
-rw-r--r-- | pretyping/typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |