From c607d496f25e98e435016e6a52f45351467f2f16 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Mar 2023 16:01:05 +0100
Subject: [PATCH] Avoid breaking invariant abstraction to establish proof mode
instance.
---
iris/base_logic/lib/invariants.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index ab012c825..d3f82d3eb 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -169,8 +169,8 @@ Section inv.
(↑N ⊆ E) True (fupd E (E ∖ ↑N)) (fupd (E ∖ ↑N) E)
(λ _ : (), (▷ P)%I) (λ _ : (), (▷ P)%I) (λ _ : (), None).
Proof.
- rewrite inv_unseal /IntoAcc /accessor bi.exist_unit.
- iIntros (?) "#Hinv _". iApply "Hinv"; done.
+ rewrite /IntoAcc /accessor bi.exist_unit.
+ iIntros (?) "#Hinv _". by iApply inv_acc.
Qed.
(** ** Derived properties *)
--
GitLab