From 859a1143ca37abdbc0129e902cbd31669788997b Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 15 Oct 2023 18:58:24 +0200 Subject: [PATCH] purge NPeano in favor of PeanoNat --- core/Verdi.v | 2 +- systems/LogCorrect.v | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) 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