From d7e80d1086f865697f045b87a03c343117978309 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 16 Dec 2021 17:01:34 +0100
Subject: [PATCH] make mono_list_auth DfracDiscarded notation consistent

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

diff --git a/iris/algebra/lib/mono_list.v b/iris/algebra/lib/mono_list.v
index df5e68c4c..dedbe3942 100644
--- a/iris/algebra/lib/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -22,7 +22,7 @@ Notation "●ML{ dq } l" :=
   (mono_list_auth dq l) (at level 20, format "●ML{ dq }  l").
 Notation "●ML{# q } l" :=
   (mono_list_auth (DfracOwn q) l) (at level 20, format "●ML{# q }  l").
-Notation "●□ML l" := (mono_list_auth DfracDiscarded l) (at level 20).
+Notation "●ML□ l" := (mono_list_auth DfracDiscarded l) (at level 20).
 Notation "●ML l" := (mono_list_auth (DfracOwn 1) l) (at level 20).
 Notation "â—¯ML l" := (mono_list_lb l) (at level 20).
 
@@ -188,7 +188,7 @@ Section mono_list_props.
   (** * Update *)
   Lemma mono_list_update {l1} l2 : l1 `prefix_of` l2 → ●ML l1 ~~> ●ML l2.
   Proof. intros ?. by apply auth_update, max_prefix_list_local_update. Qed.
-  Lemma mono_list_auth_persist dq l : ●ML{dq} l ~~> ●□ML l.
+  Lemma mono_list_auth_persist dq l : ●ML{dq} l ~~> ●ML□ l.
   Proof.
     rewrite /mono_list_auth. apply cmra_update_op; [|done].
     by apply auth_update_auth_persist.
-- 
GitLab