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

diff --git a/test-suite/success/import_mod.v b/test-suite/success/import_mod.v
index b4a8af46f..c098c6e89 100644
--- a/test-suite/success/import_mod.v
+++ b/test-suite/success/import_mod.v
@@ -1,38 +1,38 @@
 
-Definition p:=O.
-Definition m:=O.
+Definition p := 0.
+Definition m := 0.
 
 Module Test_Import.
   Module P.
-    Definition p:=(S O).
+    Definition p := 1.
   End P.
 
   Module M.
     Import P.
-    Definition m:=p.
+    Definition m := p.
   End M.
 
   Module N.
     Import M.
 
-    Lemma th0 : p=O.
-      Reflexivity.
+    Lemma th0 : p = 0.
+      reflexivity.
     Qed.
 
   End N.
 
 
   (* M and P should be closed *)
-  Lemma th1 : m=O /\ p=O.
-    Split; Reflexivity.
+  Lemma th1 : m = 0 /\ p = 0.
+    split; reflexivity.
   Qed.
 
 
   Import N.
 
   (* M and P should still be closed *)
-  Lemma th2 : m=O /\ p=O.
-    Split; Reflexivity.
+  Lemma th2 : m = 0 /\ p = 0.
+    split; reflexivity.
   Qed.
 End Test_Import.
 
@@ -42,34 +42,34 @@ End Test_Import.
 
 Module Test_Export.
   Module P.
-    Definition p:=(S O).
+    Definition p := 1.
   End P.
 
   Module M.
     Export P.
-    Definition m:=p.
+    Definition m := p.
   End M.
 
   Module N.
     Export M.
 
-    Lemma th0 : p=(S O).
-      Reflexivity.
+    Lemma th0 : p = 1.
+      reflexivity.
     Qed.
 
   End N.
 
 
   (* M and P should be closed *)
-  Lemma th1 : m=O /\ p=O.
-    Split; Reflexivity.
+  Lemma th1 : m = 0 /\ p = 0.
+    split; reflexivity.
   Qed.
 
 
   Import N.
 
   (* M and P should now be opened *)
-  Lemma th2 : m=(S O) /\ p=(S O).
-    Split; Reflexivity.
+  Lemma th2 : m = 1 /\ p = 1.
+    split; reflexivity.
   Qed.
 End Test_Export.