Réparation du cast oublié lors d'une définition castée

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@305 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 2 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1d20f928a..f73fc4f07 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -31,8 +31,14 @@ let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
 let constant_entry_of_com (com,comtypopt) =
   let sigma = Evd.empty in
   let env = Global.env() in
-    { const_entry_body = Cooked (constr_of_com sigma env com);
-      const_entry_type = option_app (constr_of_com1 true sigma env) comtypopt }
+  match comtypopt with
+      None -> 
+	{ const_entry_body = Cooked (constr_of_com sigma env com);
+	  const_entry_type = None }
+    | Some comtyp ->
+	let typ = constr_of_com_sort sigma env comtyp in
+	{ const_entry_body = Cooked (constr_of_com_casted sigma env com typ);
+	  const_entry_type = Some typ }
 
 let red_constant_entry ce = function
   | None -> ce