From aff8e8a3b8b6af7c26e00a3eab4a4c8a77b39c49 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Feb 2021 23:16:00 +0100
Subject: [PATCH] fix monPred scope binding

---
 iris/bi/monpred.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index f09bf301b..f21ce06a8 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -27,8 +27,7 @@ Record monPred :=
             monPred_mono : Proper ((âŠ‘) ==> (âŠ¢)) monPred_at }.
 Local Existing Instance monPred_mono.
 
-Declare Scope monPred.
-Bind Scope monPred with bi.
+Bind Scope bi_scope with monPred.
 
 Implicit Types P Q : monPred.
 
-- 
GitLab