From 151faf2202056fba42675672a68ef9e8a487c031 Mon Sep 17 00:00:00 2001
From: Ralf Jung <research@ralfj.de>
Date: Thu, 7 Jul 2022 16:18:48 -0400
Subject: [PATCH] fix le_upd notation

---
 iris/base_logic/lib/later_credits.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index 329c938c7..4885a108e 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -145,7 +145,7 @@ Module le_upd.
   Definition le_upd := le_upd_aux.(unseal).
   Local Definition le_upd_unseal : @le_upd = @le_upd_def := le_upd_aux.(seal_eq).
   Global Arguments le_upd {_ _} _.
-  Notation "'|==£>' P" := (le_upd P) (at level 99, P at level 200, format "|==£>  P").
+  Notation "'|==£>' P" := (le_upd P%I) (at level 99, P at level 200, format "|==£>  P") : bi_scope.
 
   Local Lemma le_upd_unfold `{!lcGS Σ} P:
     (|==£> P) ⊣⊢
-- 
GitLab