From ee20565e785bc8a3ce8e3d4f288e8b542e5119ea Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 10 Jan 2022 14:08:13 +0100
Subject: [PATCH] Fixing mono_nat problems from auto-naming.

---
 iris/base_logic/lib/mono_nat.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 8c3f670a6..184e3ddcb 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -67,8 +67,8 @@ Section mono_nat.
     unseal. iIntros "H1 H2". Typeclasses Transparent mono_nat_auth.
     iDestruct "H1" as "[H1 H1']". (* this gets annoying because mono_nat_auth = ● _ ⋅ ◯ _ *)
     iDestruct "H2" as "[H2 H2']".
-    iDestruct (own_valid_op with "H1 H2") as "[H #H']".
-    iDestruct "H'" as "[% %]". case: H0 => ->. eauto.
+    iCombineOwn "H1 H2" as "[H [%Hq %Hnm]]".
+    case: Hnm => ->. eauto.
   Qed.
   Lemma mono_nat_auth_own_exclusive γ n1 n2 :
     mono_nat_auth_own γ 1 n1 -∗ mono_nat_auth_own γ 1 n2 -∗ False.
-- 
GitLab