From ab9e5fa4037fd03529756ff045f7621be1125b11 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 10 Aug 2021 14:23:17 +0200
Subject: [PATCH] na_inv: tweak definition
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Debatable, but the proof context of `na_inv_alloc` writes `ε` instead of `CoPSet
∅`.
---
 iris/base_logic/lib/na_invariants.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index d59861a89..1f32d1134 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -23,7 +23,7 @@ Section defs.
 
   Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
     ∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧
-         inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}).
+         inv N (P ∗ own p (ε, GSet {[i]}) ∨ na_own p {[i]}).
 End defs.
 
 Global Instance: Params (@na_inv) 3 := {}.
-- 
GitLab