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
---
 toplevel/class.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 1a18e56748..e8e8653c85 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -251,12 +251,12 @@ let build_id_coercion idf_opt source =
   in
   (* juste pour verification *)
   let _ = 
-    try 
-      Reductionops.conv_leq env Evd.empty
-	(Typing.type_of env Evd.empty val_f) typ_f
-    with _ -> 
+    if not
+      (Reductionops.is_conv_leq env Evd.empty
+	(Typing.type_of env Evd.empty val_f) typ_f)
+    then
       error ("cannot be defined as coercion - "^
-	     "maybe a bad number of arguments") 
+             "maybe a bad number of arguments") 
   in
   let idf =
     match idf_opt with
-- 
cgit v1.2.3