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

diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v
index 2231e0849..97337a125 100644
--- a/test-suite/modules/obj.v
+++ b/test-suite/modules/obj.v
@@ -1,16 +1,17 @@
-Implicit Arguments On.
+Set Implicit Arguments.
+Unset Strict Implicit.
 
 Module M. 
-  Definition a:=[s:Set]s.
+  Definition a (s : Set) := s.
   Print a.
 End M.
 
 Print M.a.
 
 Module K.
-  Definition app:=[A,B:Set; f:(A->B); x:A](f x).
+  Definition app (A B : Set) (f : A -> B) (x : A) := f x.
   Module N.
-    Definition apap:=[A,B:Set](app (app 1!A 2!B)).
+    Definition apap (A B : Set) := app (app (A:=A) (B:=B)).
     Print app.
     Print apap.
   End N.
@@ -20,7 +21,6 @@ End K.
 Print K.app.
 Print K.N.apap.
 
-Module W:=K.N.
+Module W := K.N.
 
 Print W.apap.
-