diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index d2b54213a97eeb5a64c4312515d0c7780dbc13b0..6df52f94e3d0f32a7dd6976311b4380557e494b5 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -435,6 +435,8 @@ Implicit Types A : Type.
 Local Arguments uPred_holds {_} !_ _ _ /.
 Local Hint Immediate uPred_in_entails : core.
 
+(** The notations below are implicitly local due to the section, so we do not
+mind the overlap with the general BI notations. *)
 Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
 Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
 Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope.
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 5361f62d2bca051c28b083c9311cafaf5fcbd1b2..fa9af40b44ca7b0fe389c534ecfc6c03ae464bf7 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -13,9 +13,7 @@ Local Coercion siProp_holds : siProp >-> Funclass.
 Global Arguments siProp_holds : simpl never.
 Add Printing Constructor siProp.
 
-Declare Scope siProp_scope.
-Delimit Scope siProp_scope with SI.
-Bind Scope siProp_scope with siProp.
+Bind Scope bi_scope with siProp.
 
 Section cofe.
   Inductive siProp_equiv' (P Q : siProp) : Prop :=
@@ -130,17 +128,21 @@ Ltac unseal := rewrite !unseal_eqs /=.
 Section primitive.
 Local Arguments siProp_holds !_ _ /.
 
+(** The notations below are implicitly local due to the section, so we do not
+mind the overlap with the general BI notations. *)
 Notation "P ⊢ Q" := (siProp_entails P Q).
-Notation "'True'" := (siProp_pure True) : siProp_scope.
-Notation "'False'" := (siProp_pure False) : siProp_scope.
-Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : siProp_scope.
-Infix "∧" := siProp_and : siProp_scope.
-Infix "∨" := siProp_or : siProp_scope.
-Infix "→" := siProp_impl : siProp_scope.
-Notation "∀ x .. y , P" := (siProp_forall (λ x, .. (siProp_forall (λ y, P%SI)) ..)) : siProp_scope.
-Notation "∃ x .. y , P" := (siProp_exist (λ x, .. (siProp_exist (λ y, P%SI)) ..)) : siProp_scope.
-Notation "x ≡ y" := (siProp_internal_eq x y) : siProp_scope.
-Notation "â–· P" := (siProp_later P) (at level 20, right associativity) : siProp_scope.
+Notation "'True'" := (siProp_pure True) : bi_scope.
+Notation "'False'" := (siProp_pure False) : bi_scope.
+Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : bi_scope.
+Infix "∧" := siProp_and : bi_scope.
+Infix "∨" := siProp_or : bi_scope.
+Infix "→" := siProp_impl : bi_scope.
+Notation "∀ x .. y , P" :=
+  (siProp_forall (λ x, .. (siProp_forall (λ y, P%I)) ..)) : bi_scope.
+Notation "∃ x .. y , P" :=
+  (siProp_exist (λ x, .. (siProp_exist (λ y, P%I)) ..)) : bi_scope.
+Notation "x ≡ y" := (siProp_internal_eq x y) : bi_scope.
+Notation "â–· P" := (siProp_later P) : bi_scope.
 
 (** Below there follow the primitive laws for [siProp]. There are no derived laws
 in this file. *)
diff --git a/tests/siprop.ref b/tests/siprop.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/siprop.v b/tests/siprop.v
new file mode 100644
index 0000000000000000000000000000000000000000..fc72d0ccce2bfc8f9b98adb2786bcbb09867b22f
--- /dev/null
+++ b/tests/siprop.v
@@ -0,0 +1,5 @@
+From iris.si_logic Require Import bi.
+
+(** Make sure that [siProp]s are parsed in [bi_scope]. *)
+Definition test : siProp := â–· True.
+Definition testI : siPropI := â–· True.