1 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/success/NatRing.v b/test-suite/success/NatRing.v
index 6a1eeccc..8426c7e4 100644
--- a/test-suite/success/NatRing.v
+++ b/test-suite/success/NatRing.v
@@ -1,10 +1,10 @@
-Require ArithRing.
+Require Import ArithRing.
 
-Lemma l1 : (S (S O))=(plus (S O) (S O)).
-NatRing.
+Lemma l1 : 2 = 1 + 1.
+ring_nat.
 Qed.
 
-Lemma l2 : (x:nat)(S (S x))=(plus (S O) (S x)).
-Intro.
-NatRing.
-Qed.
-\ No newline at end of file
+Lemma l2 : forall x : nat, S (S x) = 1 + S x.
+intro.
+ring_nat.
+Qed.