diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index a369af8d7e573341cf9ddc527b6bed7cabbd131e..d2b54213a97eeb5a64c4312515d0c7780dbc13b0 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -115,7 +115,7 @@ Record uPred (M : ucmra) : Type := UPred {
 this way. *)
 Local Coercion uPred_holds : uPred >-> Funclass.
 Bind Scope bi_scope with uPred.
-Global Arguments uPred_holds {_} _%I _ _ : simpl never.
+Global Arguments uPred_holds {_} _ _ _ : simpl never.
 Add Printing Constructor uPred.
 Global Instance: Params (@uPred_holds) 3 := {}.
 
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 70fe83bd7df2e08324797cf89c2334bd9764e7ee..a6c66ad0b00fc88e3a6cfc064903477c7a0b199c 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -182,6 +182,7 @@ Structure bi := Bi {
   bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
                                    bi_forall bi_exist bi_sep bi_persistently bi_later;
 }.
+Bind Scope bi_scope with bi_car.
 
 Coercion bi_ofeO (PROP : bi) : ofe := Ofe PROP (bi_ofe_mixin PROP).
 Canonical Structure bi_ofeO.
@@ -204,18 +205,18 @@ Global Instance: Params (@bi_later) 1  := {}.
 Global Arguments bi_car : simpl never.
 Global Arguments bi_dist : simpl never.
 Global Arguments bi_equiv : simpl never.
-Global Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
+Global Arguments bi_entails {PROP} _ _ : simpl never, rename.
 Global Arguments bi_emp {PROP} : simpl never, rename.
 Global Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
-Global Arguments bi_and {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_or {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
+Global Arguments bi_and {PROP} _ _ : simpl never, rename.
+Global Arguments bi_or {PROP} _ _ : simpl never, rename.
+Global Arguments bi_impl {PROP} _ _ : simpl never, rename.
 Global Arguments bi_forall {PROP _} _%I : simpl never, rename.
 Global Arguments bi_exist {PROP _} _%I : simpl never, rename.
-Global Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_persistently {PROP} _%I : simpl never, rename.
-Global Arguments bi_later {PROP} _%I : simpl never, rename.
+Global Arguments bi_sep {PROP} _ _ : simpl never, rename.
+Global Arguments bi_wand {PROP} _ _ : simpl never, rename.
+Global Arguments bi_persistently {PROP} _ : simpl never, rename.
+Global Arguments bi_later {PROP} _ : simpl never, rename.
 
 Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
 Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
diff --git a/tests/bi.v b/tests/bi.v
index 92f797609a9d6fb3d00f982206b91dd3ba0f6d9a..1dc3b77c641a09563f99723825672070f96640ad 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -7,3 +7,10 @@ Proof. apply _. Qed.
 Lemma test_impl_persistent_2 `{!BiPlainly PROP} :
   Persistent (PROP:=PROP) (True → True → True).
 Proof. apply _. Qed.
+
+(* Test that the right scopes are used. *)
+Lemma test_bi_scope {PROP : bi} : True.
+Proof.
+  (* [<affine> True] is implicitly in %I scope. *)
+  pose proof (bi.wand_iff_refl (PROP:=PROP) (<affine> True)).
+Abort.