From cf31d668a077e49ca0f4a9886769b811c92a6d16 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 18 Jan 2001 23:39:09 +0000
Subject: Bug Identity Coercion

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

diff --git a/toplevel/class.ml b/toplevel/class.ml
index b6824dac78..37ef4eb925 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -265,7 +265,7 @@ let build_id_coercion idf_opt ids =
 	(Typing.type_of env Evd.empty val_f) typ_f
     with _ -> 
       error ("cannot be defined as coercion - "^
-	     "may be a bad number of arguments") 
+	     "maybe a bad number of arguments") 
   in
   let idf =
     match idf_opt with
@@ -274,8 +274,10 @@ let build_id_coercion idf_opt ids =
 	  id_of_string ("Id_"^(string_of_id ids)^"_"^
                         (string_of_class (fst (constructor_at_head t)))) 
   in
-  let constr_entry = 
-    { const_entry_body = val_f; const_entry_type = None } in
+  let constr_entry = (* Cast is necessary to express [val_f] is identity *)
+
+    { const_entry_body = mkCast (val_f, typ_f);
+      const_entry_type = None } in
   declare_constant idf (ConstantEntry constr_entry,NeverDischarge,false);
   idf
 
-- 
cgit v1.2.3