purge NPeano in favor of PeanoNat

uwplse · Oct 15, 2023 · 859a114 · 859a114
1 parent f297c02
commit 859a114
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git 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
@@ -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