diff options
author | 2004-05-14 15:43:01 +0000 | |
---|---|---|
committer | 2004-05-14 15:43:01 +0000 | |
commit | fbdbbd2cea72f5f2d9d677ca466ceed63d969e33 (patch) | |
tree | e49bbe4cd20233beb1b348f30671ad0a641d1045 /pretyping/typing.ml | |
parent | e18b8de00962f830052b169c04c753b830d60594 (diff) |
test de conversion laissait echapper exception NotConvertible
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5746 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typing.ml')
-rw-r--r-- | pretyping/typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index fc4b50ed2..b41947d30 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -113,7 +113,7 @@ 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 _ = judge_of_cast env j1 j2 in let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in let j3 = execute mf env1 sigma c3 in judge_of_letin env name j1 j2 j3 |