Merge pull request #54 from SkySkimmer/replaceby

Fix incorrect "replace by"
mit-pdos · Sep 28, 2023 · 7e7751c · 7e7751c
2 parents d6b4b3e + 46e0191
commit 7e7751c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/program_proof/wal/recovery_proof.v b/src/program_proof/wal/recovery_proof.v
@@ -1331,7 +1331,7 @@ Proof.
             rewrite Nat.max_l; last by lia.
             iApply "Hdurable_lb_pos".
           }
-          replace (slidingM.memEnd _) with (int.Z diskEnd) by reflexivity.
+          replace (slidingM.memEnd _) with (int.Z diskEnd) by assumption.
           iSplit.
           {
             iPureIntro.