Prise en compte des '?' aussi dans le type des définitions

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

1 files changed, 6 insertions, 2 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0ff52efda..400f12fa2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -33,6 +33,7 @@ open Nametab
 open Typeops
 open Indtypes
 
+let mkCastC(a,b) = ope("CAST",[a;b])
 let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some x,b)])
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
 let mkProdC (x,a,b) = ope("PROD",[a;slam(Some x,b)])
@@ -51,8 +52,11 @@ let constant_entry_of_com (com,comtypopt,opacity) =
 	  const_entry_type = None;
           const_entry_opaque = opacity }
     | Some comtyp ->
-	let typ = interp_type sigma env comtyp in
-	{ const_entry_body = interp_casted_constr sigma env com typ;
+	(* We use a cast to avoid troubles with evars in comtyp *)
+	(* that can only be resolved knowing com *)
+	let b = mkCastC (com,comtyp) in
+	let (body,typ) = destCast (interp_constr sigma env b) in
+	{ const_entry_body = body;
 	  const_entry_type = Some typ;
           const_entry_opaque = opacity }