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, 16 insertions, 16 deletions

diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v
index 13c284181..8dadace77 100644
--- a/test-suite/modules/Tescik.v
+++ b/test-suite/modules/Tescik.v
@@ -1,30 +1,30 @@
 
 Module Type ELEM.
-  Parameter A:Set.
-  Parameter x:A.
+  Parameter A : Set.
+  Parameter x : A.
 End ELEM.
 
 Module Nat.
-    Definition A:=nat.
-    Definition x:=O.
+    Definition A := nat.
+    Definition x := 0.
 End Nat. 
 
-Module List[X:ELEM].
-  Inductive list : Set := nil : list 
-		       | cons : X.A -> list -> list.
+Module List (X: ELEM).
+  Inductive list : Set :=
+    | nil : list
+    | cons : X.A -> list -> list.
  
-  Definition head := 
-     [l:list]Cases l of 
-	  nil => X.x 
-	| (cons x _) => x
-     end.
+  Definition head (l : list) := match l with
+                                | nil => X.x
+                                | cons x _ => x
+                                end.
 
-  Definition singl := [x:X.A] (cons x nil).
+  Definition singl (x : X.A) := cons x nil.
   
-  Lemma head_singl : (x:X.A)(head (singl x))=x.
-  Auto.
+  Lemma head_singl : forall x : X.A, head (singl x) = x.
+  auto.
   Qed.
 
 End List.
 
-Module N:=(List Nat).
+Module N := List Nat.
\ No newline at end of file