Merge pull request #141 from uwplse/purge-npeano

purge NPeano in favor of PeanoNat
uwplse · Oct 15, 2023 · f31f907 · f31f907
2 parents f297c02 + 859a114
commit f31f907
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