From 9a75bfec45650d7b95288125d6e00777c890bc25 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 29 Nov 2000 17:13:46 +0000
Subject: Suppression cast inutile

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1033 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/class.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/toplevel/class.ml b/toplevel/class.ml
index e6e4654b56..7b803fb4d6 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -244,11 +244,11 @@ let build_id_coercion idf_opt ids =
       (mkProd (Anonymous, applistc vs (rel_list 0 llams), lift 1 t))
       lams
   in
-  let constr_f = mkCast (val_f, typ_f) in
   (* juste pour verification *)
   let _ = 
     try 
-      Typing.type_of env Evd.empty constr_f
+      Reduction.conv_leq env Evd.empty
+	(Typing.type_of env Evd.empty val_f) typ_f
     with _ -> 
       error ("cannot be defined as coercion - "^
 	     "may be a bad number of arguments") 
@@ -261,7 +261,7 @@ let build_id_coercion idf_opt ids =
                         (string_of_cl (fst (constructor_at_head t)))) 
   in
   let constr_entry = 
-    { const_entry_body = constr_f; const_entry_type = None } in
+    { const_entry_body = val_f; const_entry_type = None } in
   declare_constant idf (ConstantEntry constr_entry,NeverDischarge);
   idf
 
-- 
cgit v1.2.3