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

4 files changed, 22 insertions, 20 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
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 499c06606..ccd92f696 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -31,10 +31,11 @@ Type
 (* Interaction with coercions *)
 Parameter bool2nat : bool -> nat.
 Coercion bool2nat : bool >-> nat.
-Check (fun x => match x with
-                | O => true
-                | S _ => 0
-                end:nat).
+Definition foo : nat -> nat :=
+  fun x => match x with
+             | O => true
+             | S _ => 0
+           end.
 
 (****************************************************************************)
 (* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v   *)
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 82c5cf2e7..dd84402df 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -9,13 +9,11 @@
 (************************************************************************)
 
 Lemma essai : forall x : nat, x = x.
-
  refine
  ((fun x0 : nat => match x0 with
                    | O => _
                    | S p => _
-                   end)
-  :forall x : nat, x = x).  (* x0=x0 et x0=x0 *)
+                   end)).
 
 Restart.
 
@@ -145,11 +143,10 @@ Lemma essai : forall n : nat, {x : nat | x = S n}.
 Restart.
 
  refine
- ((fun n : nat => match n with
+   (fun n : nat => match n with
                   | O => _
                   | S p => _
-                  end)
-  :forall n : nat, {x : nat | x = S n}).
+                  end).
 
 Restart.
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5d144f196..5cccc225c 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;