diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 0e9f1eb97ef4835c8748da1705334a94ce7cc94f..965811c87ff974cd6a9cd32fd6c51bece7ca9710 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.