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, 6 insertions, 5 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7400cdd9c..2921cd536 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -558,7 +558,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
 	  let pred = nf_evar (evars_of !evdref) pred in
 	  let p = nf_evar (evars_of !evdref) p in
-	 (*   msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
 	  let f cs b =
 	    let n = rel_context_length cs.cs_args in
 	    let pi = lift n pred in (* liftn n 2 pred ? *)
@@ -575,7 +574,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		cs.cs_args
 	    in
 	    let env_c = push_rels csgn env in 
-(* 	      msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
 	    let bj = pretype (mk_tycon pi) env_c evdref lvar b in
 	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
 	  let b1 = f cstrs.(0) b1 in
@@ -600,9 +598,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj
 	    | CastConv (k,t) ->
 		let tj = pretype_type empty_valcon env evdref lvar t in
-		let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in
-		  (* User Casts are for helping pretyping, experimentally not to be kept*)
-		  (* ... except for Correctness *)
+ 		let cj = pretype empty_tycon env evdref lvar c in
+		let cj = match k with
+		  | VMcast when not (occur_existential cj.uj_type || occur_existential tj.utj_val) ->
+		      ignore (Reduction.vm_conv Reduction.CUMUL env cj.uj_type tj.utj_val); cj
+		  | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tj.utj_val)
+		in
 		let v = mkCast (cj.uj_val, k, tj.utj_val) in
 		  { uj_val = v; uj_type = tj.utj_val }
 	in inh_conv_coerce_to_tycon loc env evdref cj tycon