From 528ac5ec36a9a4c176ca45cf8aaf36e45e12d0b8 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Fri, 2 Jun 2023 15:32:42 +0200
Subject: [PATCH] Remove unneeded @uPredI M

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

diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index ba7a2e4f2..b44fb1ef8 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -93,7 +93,7 @@ Section upred.
     Proof. by uPred.unseal. Qed.
 
     Lemma reservation_map_data_validI k b :
-      ✓ reservation_map_data k b ⊣⊢@{uPredI M} ✓ b.
+      ✓ reservation_map_data k b ⊣⊢ ✓ b.
     Proof.
       rewrite reservation_validI /= singleton_validI.
       apply (anti_symm _); first by rewrite bi.and_elim_l.
-- 
GitLab