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

4 files changed, 109 insertions, 113 deletions

diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v
index bba356f2d..6fd0fe8b6 100644
--- a/test-suite/ideal-features/Apply.v
+++ b/test-suite/ideal-features/Apply.v
@@ -6,21 +6,25 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This needs unification on type *)
+(* This needs step by step unfolding *)
 
-Goal (n,m:nat)(eq nat (S m) (S n)).
-Intros.
-Apply f_equal.
+Fixpoint T (n:nat) : Prop :=
+  match n with
+  | O => True
+  | S p => n = n -> T p
+  end.
 
-(* f_equal : (A,B:Set; f:(A->B); x,y:A)x=y->(f x)=(f y) *)
-(* and A cannot be deduced from the goal but only from the type of f, x or y *)
+Require Import Arith.
 
+Goal T 3 -> T 1.
+intro H.
+apply H.
 
-(* This needs step by step unfolding *)
+(* This needs unification on type *)
 
-Fixpoint T [n:nat] : Prop := Cases n of O => True | (S p) => n=n->(T p) end.
-Require Arith.
+Goal forall n m : nat, S m = S n :>nat.
+intros.
+apply f_equal.
 
-Goal (T (3))->(T (1)).
-Intro H.
-Apply H.
+(* f_equal : forall (A B:Set) (f:A->B) (x y:A), x=y->(f x)=(f y) *)
+(* and A cannot be deduced from the goal but only from the type of f, x or y *)
diff --git a/test-suite/ideal-features/Case3.v b/test-suite/ideal-features/Case3.v
index e9dba1e3f..de7784aec 100644
--- a/test-suite/ideal-features/Case3.v
+++ b/test-suite/ideal-features/Case3.v
@@ -1,28 +1,29 @@
-Inductive Le : nat->nat->Set :=
-  LeO: (n:nat)(Le O n) 
-| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)).
+Inductive Le : nat -> nat -> Set :=
+  | LeO : forall n : nat, Le 0 n
+  | LeS : forall n m : nat, Le n m -> Le (S n) (S m).
 
-Parameter iguales : (n,m:nat)(h:(Le n m))Prop .
+Parameter discr_l : forall n : nat, S n <> 0.
 
-Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of 
-                         (LeO O) => True
-                       | (LeS (S x) (S y) H) => (iguales (S x) (S y) H)
-                       | _ => False end.
+Type
+  (fun n : nat =>
+   match n return (n = 0 \/ n <> 0) with
+   | O => or_introl (0 <> 0) (refl_equal 0)
+   | S O => or_intror (1 = 0) (discr_l 0)
+   | S (S x) => or_intror (S (S x) = 0) (discr_l (S x))
+   end).
 
+Parameter iguales : forall (n m : nat) (h : Le n m), Prop.
 
-Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of 
-                         (LeO O) => True
-                       | (LeS (S x) O H) => (iguales (S x) O H)
-                       | _ => False end.
-
-Parameter discr_l : (n:nat) ~((S n)=O).
-
-Type 
-[n:nat] 
-  <[n:nat]n=O\/~n=O>Cases n of 
-      O     => (or_introl ? ~O=O (refl_equal ? O))      
-   |  (S O) => (or_intror (S O)=O ? (discr_l O))
-   |  (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x)))
- 
+Type
+  match LeO 0 as h in (Le n m) return Prop with
+  | LeO O => True
+  | LeS (S x) (S y) H => iguales (S x) (S y) H
+  | _ => False
   end.
 
+Type
+  match LeO 0 as h in (Le n m) return Prop with
+  | LeO O => True
+  | LeS (S x) O H => iguales (S x) 0 H
+  | _ => False
+  end.
diff --git a/test-suite/ideal-features/Case4.v b/test-suite/ideal-features/Case4.v
index d8f14a4e1..cb076a718 100644
--- a/test-suite/ideal-features/Case4.v
+++ b/test-suite/ideal-features/Case4.v
@@ -1,39 +1,34 @@
-Inductive listn : nat-> Set := 
-  niln : (listn O) 
-| consn : (n:nat)nat->(listn n) -> (listn (S n)).
-
-Inductive empty : (n:nat)(listn n)-> Prop := 
-  intro_empty: (empty O niln).
-
-Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)).
-
-Type 
-[n:nat] [l:(listn n)]
-  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
-        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
-   |  ((consn n O y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n O y))
-   |  ((consn n a y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n a y))
-
-  end.
-
-
-Type 
-[n:nat] [l:(listn n)]
-  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
-        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
-   |  (consn n O y)  =>  (or_intror (empty (S n) (consn n O y)) ? 
-                                              (inv_empty n O y))
-   |  (consn n a y) =>  (or_intror (empty (S n) (consn n a y)) ? 
-                                          (inv_empty n a y))
-
-  end.
-
-Type 
-[n:nat] [l:(listn n)]
-  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
-        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
-   |  ((consn O a y) as b) =>  (or_intror (empty (S O) b) ? (inv_empty O a y))
-   |  ((consn n a y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n a y))
-
-  end.
-
+Inductive listn : nat -> Set :=
+  | niln : listn 0
+  | consn : forall n : nat, nat -> listn n -> listn (S n).
+
+Inductive empty : forall n : nat, listn n -> Prop :=
+    intro_empty : empty 0 niln.
+
+Parameter
+  inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l).
+
+Type
+  (fun (n : nat) (l : listn n) =>
+   match l in (listn n) return (empty n l \/ ~ empty n l) with
+   | niln => or_introl (~ empty 0 niln) intro_empty
+   | consn n O y as b => or_intror (empty (S n) b) (inv_empty n 0 y)
+   | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
+   end).
+
+
+Type
+  (fun (n : nat) (l : listn n) =>
+   match l in (listn n) return (empty n l \/ ~ empty n l) with
+   | niln => or_introl (~ empty 0 niln) intro_empty
+   | consn n O y => or_intror (empty (S n) (consn n 0 y)) (inv_empty n 0 y)
+   | consn n a y => or_intror (empty (S n) (consn n a y)) (inv_empty n a y)
+   end).
+
+Type
+  (fun (n : nat) (l : listn n) =>
+   match l in (listn n) return (empty n l \/ ~ empty n l) with
+   | niln => or_introl (~ empty 0 niln) intro_empty
+   | consn O a y as b => or_intror (empty 1 b) (inv_empty 0 a y)
+   | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
+   end).
diff --git a/test-suite/ideal-features/Case8.v b/test-suite/ideal-features/Case8.v
index 73b55028d..2ac5bd8c0 100644
--- a/test-suite/ideal-features/Case8.v
+++ b/test-suite/ideal-features/Case8.v
@@ -1,40 +1,36 @@
-Inductive listn : nat-> Set := 
-  niln : (listn O) 
-| consn : (n:nat)nat->(listn n) -> (listn (S n)).
-
-Inductive empty : (n:nat)(listn n)-> Prop := 
-  intro_empty: (empty O niln).
-
-Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)).
-
-Type 
-[n:nat] [l:(listn n)]
-  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
-        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
-   |  ((consn n O y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n O y))
-   |  ((consn n a y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n a y))
-
-  end.
-
-
-Type 
-[n:nat] [l:(listn n)]
-  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
-        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
-   |  (consn n O y)  =>  (or_intror (empty (S n) (consn n O y)) ? 
-                                              (inv_empty n O y))
-   |  (consn n a y) =>  (or_intror (empty (S n) (consn n a y)) ? 
-                                          (inv_empty n a y))
-
-  end.
-
-
-
-Type 
-[n:nat] [l:(listn n)]
-  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
-        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
-   |  ((consn O a y) as b) =>  (or_intror (empty (S O) b) ? (inv_empty O a y))
-   |  ((consn n a y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n a y))
-
-  end.
+Inductive listn : nat -> Set :=
+  | niln : listn 0
+  | consn : forall n : nat, nat -> listn n -> listn (S n).
+
+Inductive empty : forall n : nat, listn n -> Prop :=
+    intro_empty : empty 0 niln.
+
+Parameter
+  inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l).
+
+Type
+  (fun (n : nat) (l : listn n) =>
+   match l in (listn n) return (empty n l \/ ~ empty n l) with
+   | niln => or_introl (~ empty 0 niln) intro_empty
+   | consn n O y as b => or_intror (empty (S n) b) (inv_empty n 0 y)
+   | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
+   end).
+
+
+Type
+  (fun (n : nat) (l : listn n) =>
+   match l in (listn n) return (empty n l \/ ~ empty n l) with
+   | niln => or_introl (~ empty 0 niln) intro_empty
+   | consn n O y => or_intror (empty (S n) (consn n 0 y)) (inv_empty n 0 y)
+   | consn n a y => or_intror (empty (S n) (consn n a y)) (inv_empty n a y)
+   end).
+
+
+
+Type
+  (fun (n : nat) (l : listn n) =>
+   match l in (listn n) return (empty n l \/ ~ empty n l) with
+   | niln => or_introl (~ empty 0 niln) intro_empty
+   | consn O a y as b => or_intror (empty 1 b) (inv_empty 0 a y)
+   | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
+   end).