diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index f09bf301bf72cc17aec70439030e9b23519a2eb8..f21ce06a80e578db89012d07fb7d5452f4cc853e 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.