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, 11 deletions

diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v
index fb734b5d5..9657c685d 100644
--- a/test-suite/modules/grammar.v
+++ b/test-suite/modules/grammar.v
@@ -1,15 +1,15 @@
 Module N.
-Definition f:=plus.
-Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E].
-Check (f O O).
+Definition f := plus.
+(* <Warning> : Syntax is discontinued *)
+Check (f 0 0).
 End N.
-Check (N.f O O).
+Check (N.f 0 0).
 Import N.
-Check (N.f O O).
-Check (f O O).
-Module M:=N.
-Check (f O O).
-Check (N.f O O).
+Check (f 0 0).
+Check (f 0 0).
+Module M := N.
+Check (f 0 0).
+Check (f 0 0).
 Import M.
-Check (f O O).
-Check (N.f O O).
+Check (f 0 0).
+Check (N.f 0 0).
\ No newline at end of file