From 12a13c739a71cb4e796cc9e6e1596bb75be4ff1c Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 7 Nov 2008 18:22:08 +0000
Subject: 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
---
 pretyping/pretyping.ml          | 11 ++++++-----
 test-suite/success/Cases.v      |  9 +++++----
 test-suite/success/TestRefine.v |  9 +++------
 toplevel/command.ml             | 13 ++++++++-----
 4 files changed, 22 insertions(+), 20 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7400cdd9ce..2921cd5365 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 499c066064..ccd92f6960 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 82c5cf2e74..dd84402dfa 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 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;
-- 
cgit v1.2.3