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
---
 test-suite/success/Cases.v      | 9 +++++----
 test-suite/success/TestRefine.v | 9 +++------
 2 files changed, 8 insertions(+), 10 deletions(-)

(limited to 'test-suite')

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.
 
-- 
cgit v1.2.3