diff --git a/core/Verdi.v b/core/Verdi.v
index c84a3aa9..73dcc63e 100644
--- a/core/Verdi.v
+++ b/core/Verdi.v
@@ -11,4 +11,4 @@ Require Export StructTact.StructTactics.
 Require Export Verdi.VerdiHints.
 Require Export Verdi.Net.
 
-Require NPeano.
+Require PeanoNat.
diff --git a/systems/LogCorrect.v b/systems/LogCorrect.v
index 32cedf11..68833a8a 100644
--- a/systems/LogCorrect.v
+++ b/systems/LogCorrect.v
@@ -68,7 +68,7 @@ Section LogCorrect.
           end.
           rewrite app_length.
           simpl.
-          rewrite NPeano.Nat.add_1_r.
+          rewrite Nat.add_1_r.
           reflexivity.
       + break_match.
         * find_inversion.
@@ -85,7 +85,7 @@ Section LogCorrect.
         end.
         rewrite app_length.
         simpl.
-        rewrite NPeano.Nat.add_1_r.
+        rewrite Nat.add_1_r.
         reflexivity.
       + rewrite apply_log_app.
         match goal with
@@ -127,7 +127,7 @@ Section LogCorrect.
           end.
           rewrite app_length.
           simpl.
-          rewrite NPeano.Nat.add_1_r.
+          rewrite Nat.add_1_r.
           reflexivity.
       + break_match.
         * find_inversion.
@@ -144,7 +144,7 @@ Section LogCorrect.
         end.
         rewrite app_length.
         simpl.
-        rewrite NPeano.Nat.add_1_r.
+        rewrite Nat.add_1_r.
         reflexivity.
       + rewrite apply_log_app.
         match goal with