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, 43 insertions, 45 deletions

diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index c324919ff..6df2f83d1 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -1,40 +1,38 @@
 
-Require Omega.
+Require Import Omega.
 
 (* Submitted by Xavier Urbain 18 Jan 2002 *)
 
-Lemma lem1 : (x,y:Z) 
-  `-5 < x < 5` ->
-  `-5 < y` ->
-  `-5 < x+y+5`.
+Lemma lem1 :
+ forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z.
 Proof.
-Intros x y.
-Omega.
+intros x y.
+ omega.
 Qed.
 
 (* Proposed by Pierre Crégut *)
 
-Lemma lem2 : (x:Z) `x < 4` -> `x > 2` -> `x=3`.
-Intro.
-Omega.
+Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z.
+intro.
+ omega.
 Qed.
 
 (* Proposed by Jean-Christophe Filliâtre *)
 
-Lemma lem3 : (x,y:Z) `x = y` -> `x+x = y+y`.
+Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
 Proof.
-Intros.
-Omega.
+intros.
+ omega.
 Qed.
 
 (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
 (* internal variable and a section variable (June 2001) *)
 
 Section A.
-Variable x,y : Z.
-Hypothesis H : `x > y`.
-Lemma lem4 : `x > y`.
-Omega.
+Variable x y : Z.
+Hypothesis H : (x > y)%Z.
+Lemma lem4 : (x > y)%Z.
+ omega.
 Qed.
 End A.
 
@@ -42,48 +40,48 @@ End A.
 (* May 2002 *)
 
 Section B.
-Variables R1,R2,S1,S2,H,S:Z.
-Hypothesis I:`R1 < 0`->`R2 = R1+(2*S1-1)`.
-Hypothesis J:`R1 < 0`->`S2 = S1-1`.
-Hypothesis K:`R1 >= 0`->`R2 = R1`.
-Hypothesis L:`R1 >= 0`->`S2 = S1`.
-Hypothesis M:`H <= 2*S`.
-Hypothesis N:`S < H`.
-Lemma lem5 : `H > 0`.
-Omega.
+Variable R1 R2 S1 S2 H S : Z.
+Hypothesis I : (R1 < 0)%Z -> R2 = (R1 + (2 * S1 - 1))%Z.
+Hypothesis J : (R1 < 0)%Z -> S2 = (S1 - 1)%Z.
+Hypothesis K : (R1 >= 0)%Z -> R2 = R1.
+Hypothesis L : (R1 >= 0)%Z -> S2 = S1.
+Hypothesis M : (H <= 2 * S)%Z.
+Hypothesis N : (S < H)%Z.
+Lemma lem5 : (H > 0)%Z.
+ omega.
 Qed.
 End B.
 
 (* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *)
-Lemma lem6: (A: Set) (i:Z) `i<= 0` -> (`i<= 0` -> A) -> `i<=0`.
-Intros.
-Omega.
+Lemma lem6 :
+ forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z.
+intros.
+ omega.
 Qed.
 
 (* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
-Require Omega.
+Require Import Omega.
 Section C.
-Parameter g:(m:nat)~m=O->Prop.
-Parameter f:(m:nat)(H:~m=O)(g m H).
-Variable n:nat.
-Variable ap_n:~n=O.
-Local delta:=(f n ap_n).
-Lemma lem7 : n=n.
-Omega.
+Parameter g : forall m : nat, m <> 0 -> Prop.
+Parameter f : forall (m : nat) (H : m <> 0), g m H.
+Variable n : nat.
+Variable ap_n : n <> 0.
+Let delta := f n ap_n.
+Lemma lem7 : n = n.
+ omega.
 Qed.
 End C.
 
 (* Problem of dependencies *)
-Require Omega.
-Lemma lem8 : (H:O=O->O=O) H=H -> O=O.
-Intros; Omega.
+Require Import Omega.
+Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
+intros;  omega.
 Qed.
 
 (* Bug that what caused by the use of intro_using in Omega *)
-Require Omega.
-Lemma lem9 : (p,q:nat)
-  ~((le p q)/\(lt p q)\/(le q p)/\(lt p q))
-  -> (lt p p)\/(le p p).
-Intros; Omega.
+Require Import Omega.
+Lemma lem9 :
+ forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p.
+intros;  omega.
 Qed.