Slight change of the semantics of user-given casts: they don't really

help the type _checking_ anymore (they don't become typing constraints)
but they permit to coerce a subterm in a type. In particular, when
using a VM cast we avoid unneeded, unexpected conversions using the
default machine (oops!). Also remove the corresponding comment in
pretyping and fix the wrong use of casts in toplevel/command: accept
the trouble of using evars. This has the somewhat adverse effect that
when typing casted object we now have no typing constraints (see
e.g. examples in Cases.v)!
Probably, this will be backtracked partially tomorrow as many contribs
can rely on it and the change could make some unifications fail (in
particular with deep coercions). Let's try anyway!


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

1 files changed, 8 insertions, 5 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5d144f1961..5cccc225cd 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -113,11 +113,14 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
           const_entry_opaque = opacity;
 	  const_entry_boxed = boxed }
     | Some comtyp ->
-	(* We use a cast to avoid troubles with evars in comtyp *)
-	(* that can only be resolved knowing com *)
-	let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv (DEFAULTcast,comtyp))) bl in
-	let b, imps = interp_constr_evars_impls env b in
-	let (body,typ) = destSubCast b in
+	let ty = generalize_constr_expr comtyp bl in
+	let b = abstract_constr_expr com bl in
+	let evdref = ref (Evd.create_evar_defs Evd.empty) in
+	let ty, impls = interp_type_evars_impls ~evdref env ty in
+	let b, imps = interp_casted_constr_evars_impls ~evdref env b ty in
+	let body, typ = nf_isevar !evdref b, nf_isevar !evdref ty in
+	  check_evars env Evd.empty !evdref body;
+	  check_evars env Evd.empty !evdref typ;
 	  imps,
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;