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, 12 insertions, 14 deletions

diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
index 58ae2a52d..9d24d6ce4 100644
--- a/test-suite/modules/modul.v
+++ b/test-suite/modules/modul.v
@@ -1,18 +1,17 @@
 Module M.
-  Parameter rel:nat -> nat -> Prop.
+  Parameter rel : nat -> nat -> Prop.
 
-  Axiom w : (n:nat)(rel O (S n)).
+  Axiom w : forall n : nat, rel 0 (S n).
 
-  Hints Resolve w.
+  Hint Resolve w.
 
-  Grammar constr constr8 := 
-     not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ].
+  (* <Warning> : Grammar is replaced by Notation *)
   
   Print Hint *.
 
-  Lemma w1 : (O#(S O)).
-  Auto.
-  Save.
+  Lemma w1 : rel 0 1.
+  auto.
+  Qed.
 
 End M.
 
@@ -24,14 +23,13 @@ Auto.
 
 Import M.
 
-Lemma w1 : (O#(S O)).
-Auto.
-Save.
+Lemma w1 : rel 0 1.
+auto.
+Qed.
 
-Check (O#O).
+Check (rel 0 0).
 Locate rel.
 
 Locate Module M.
 
-Module N:=Top.M.
-
+Module N := Top.M.