1 files changed, 18 insertions, 18 deletions
diff --git a/test-suite/success/import_mod.v b/test-suite/success/import_mod.v
index b4a8af46..c098c6e8 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.