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

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   *)