From 46e01918e3c32f50685f17f13a15f34e2bc0975f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 28 Sep 2023 13:32:44 +0200 Subject: [PATCH] Fix incorrect "replace by" Before Coq 8.19 `replace foo with bar by tac` actually meant `replace foo with bar by first [assumption | symmetry; assumption | tac]`. --- src/program_proof/wal/recovery_proof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/program_proof/wal/recovery_proof.v b/src/program_proof/wal/recovery_proof.v index f28bd08b4..8cbb20433 100644 --- 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.