From fbdbbd2cea72f5f2d9d677ca466ceed63d969e33 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 14 May 2004 15:43:01 +0000
Subject: 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
---
 pretyping/typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index fc4b50ed26..b41947d308 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
-- 
cgit v1.2.3