From 70c2e721de31019618a20eb10ced696ac8b94f8d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 8 Aug 2022 15:05:39 +0000
Subject: [PATCH] use notation

---
 iris/algebra/auth.v | 2 +-
 iris/algebra/view.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 3166745c3..82b2cabc0 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -131,7 +131,7 @@ Section auth.
   Lemma auth_frag_core a : core (â—¯ a) = â—¯ (core a).
   Proof. apply view_frag_core. Qed.
   Lemma auth_both_core_discarded a b :
-    core (●{DfracDiscarded} a ⋅ ◯ b) ≡ ●{DfracDiscarded} a ⋅ ◯ (core b).
+    core (●□ a ⋅ ◯ b) ≡ ●□ a ⋅ ◯ (core b).
   Proof. apply view_both_core_discarded. Qed.
   Lemma auth_both_core_frac q a b :
     core (●{#q} a ⋅ ◯ b) ≡ ◯ (core b).
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index cca42710d..0406fc976 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -296,7 +296,7 @@ Section cmra.
   Lemma view_frag_core b : core (â—¯V b) = â—¯V (core b).
   Proof. done. Qed.
   Lemma view_both_core_discarded a b :
-    core (●V{DfracDiscarded} a ⋅ ◯V b) ≡ ●V{DfracDiscarded} a ⋅ ◯V (core b).
+    core (●V□ a ⋅ ◯V b) ≡ ●V□ a ⋅ ◯V (core b).
   Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
   Lemma view_both_core_frac q a b :
     core (●V{#q} a ⋅ ◯V b) ≡ ◯V (core b).
-- 
GitLab