Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 6 deletions

diff --git a/test-suite/success/Case14.v b/test-suite/success/Case14.v
index edecee79e..f106a64cb 100644
--- a/test-suite/success/Case14.v
+++ b/test-suite/success/Case14.v
@@ -4,13 +4,18 @@
 Axiom bad : false = true.
 
 Definition try1 : False :=
-  <[b:bool][_:false=b](if b then False else True)>
-  Cases bad of refl_equal => I end.
+  match bad in (_ = b) return (if b then False else True) with
+  | refl_equal => I
+  end.
 
 Definition try2 : False :=
-  <[b:bool][_:false=b]((if b then False else True)::Prop)>
-  Cases bad of refl_equal => I end.
+  match bad in (_ = b) return ((if b then False else True):Prop) with
+  | refl_equal => I
+  end.
 
 Definition try3 : False :=
-  <[b:bool][_:false=b](([b':bool] if b' then False else True) b)>
-  Cases bad of refl_equal => I end.
+  match
+    bad in (_ = b) return ((fun b' : bool => if b' then False else True) b)
+  with
+  | refl_equal => I
+  end.