diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index b2c883411a41b6878fc1c06573aa7d0db9d47c35..b7affdfdcde81325d24fbf8f3fbb9c867c562b9b 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -7,29 +7,29 @@ Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (** Notations for unary variants *)
 Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
-  (big_opL bi_sep (λ k x, P) l) : bi_scope.
+  (big_opL bi_sep (λ k x, P%I) l) : bi_scope.
 Notation "'[∗' 'list]' x ∈ l , P" :=
-  (big_opL bi_sep (λ _ x, P) l) : bi_scope.
-Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope.
+  (big_opL bi_sep (λ _ x, P%I) l) : bi_scope.
+Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps%I) : bi_scope.
 
 Notation "'[∧' 'list]' k ↦ x ∈ l , P" :=
-  (big_opL bi_and (λ k x, P) l) : bi_scope.
+  (big_opL bi_and (λ k x, P%I) l) : bi_scope.
 Notation "'[∧' 'list]' x ∈ l , P" :=
-  (big_opL bi_and (λ _ x, P) l) : bi_scope.
-Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps) : bi_scope.
+  (big_opL bi_and (λ _ x, P%I) l) : bi_scope.
+Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps%I) : bi_scope.
 
 Notation "'[∨' 'list]' k ↦ x ∈ l , P" :=
-  (big_opL bi_or (λ k x, P) l) : bi_scope.
+  (big_opL bi_or (λ k x, P%I) l) : bi_scope.
 Notation "'[∨' 'list]' x ∈ l , P" :=
-  (big_opL bi_or (λ _ x, P) l) : bi_scope.
-Notation "'[∨]' Ps" := (big_opL bi_or (λ _ x, x) Ps) : bi_scope.
+  (big_opL bi_or (λ _ x, P%I) l) : bi_scope.
+Notation "'[∨]' Ps" := (big_opL bi_or (λ _ x, x) Ps%I) : bi_scope.
 
-Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m) : bi_scope.
-Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m) : bi_scope.
+Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P%I) m) : bi_scope.
+Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P%I) m) : bi_scope.
 
-Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X) : bi_scope.
+Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P%I) X) : bi_scope.
 
-Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scope.
+Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P%I) X) : bi_scope.
 
 (** Definitions and notations for binary variants *)
 (** A version of the separating big operator that ranges over two lists. This
@@ -47,9 +47,9 @@ Global Instance: Params (@big_sepL2) 3 := {}.
 Global Arguments big_sepL2 {PROP A B} _ !_ !_ /.
 Typeclasses Opaque big_sepL2.
 Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
-  (big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope.
+  (big_sepL2 (λ k x1 x2, P%I) l1 l2) : bi_scope.
 Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
-  (big_sepL2 (λ _ x1 x2, P) l1 l2) : bi_scope.
+  (big_sepL2 (λ _ x1 x2, P%I) l1 l2) : bi_scope.
 
 Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
     (Φ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP :=
@@ -61,9 +61,9 @@ Global Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
 Definition big_sepM2_eq : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
 Global Instance: Params (@big_sepM2) 6 := {}.
 Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
-  (big_sepM2 (λ k x1 x2, P) m1 m2) : bi_scope.
+  (big_sepM2 (λ k x1 x2, P%I) m1 m2) : bi_scope.
 Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P" :=
-  (big_sepM2 (λ _ x1 x2, P) m1 m2) : bi_scope.
+  (big_sepM2 (λ _ x1 x2, P%I) m1 m2) : bi_scope.
 
 (** * Properties *)
 Section big_op.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 5447c68eda4f7a0b43edd8fe4fc15f1f03a6074b..70fe83bd7df2e08324797cf89c2334bd9764e7ee 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -249,9 +249,9 @@ Infix "∗" := bi_sep : bi_scope.
 Notation "(∗)" := bi_sep (only parsing) : bi_scope.
 Notation "P -∗ Q" := (bi_wand P Q) : bi_scope.
 Notation "∀ x .. y , P" :=
-  (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.
+  (bi_forall (λ x, .. (bi_forall (λ y, P%I)) ..)) : bi_scope.
 Notation "∃ x .. y , P" :=
-  (bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope.
+  (bi_exist (λ x, .. (bi_exist (λ y, P%I)) ..)) : bi_scope.
 Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
 
 Notation "â–· P" := (bi_later P) : bi_scope.
diff --git a/tests/iris_notation.ref b/tests/iris_notation.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/iris_notation.v b/tests/iris_notation.v
new file mode 100644
index 0000000000000000000000000000000000000000..3e6fb553694c636e6256ff94da9f05e231c5e512
--- /dev/null
+++ b/tests/iris_notation.v
@@ -0,0 +1,45 @@
+From iris.algebra Require Import frac.
+From iris.proofmode Require Import tactics monpred.
+From iris.base_logic Require Import base_logic lib.fancy_updates.
+
+Section base_logic_tests.
+  Context {M : ucmra}.
+  Implicit Types P Q R : uPred M.
+
+  (* Test scopes for bupd *)
+  Definition use_bupd_uPred (n : nat) : uPred M :=
+    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.
+  Definition use_plainly_uPred (n : nat) : uPred M :=
+    ■ |==> ∃ m : nat , ⌜ n = 2 ⌝.
+
+  (* Test scopes inside big-ops *)
+  Definition big_op_scope_uPred_1 (xs : list nat) : uPred M :=
+    [∗ list] _ ↦ x ∈ xs, True.
+  Definition big_op_scope_uPred_2 (xs : list nat) : uPred M :=
+    [∗ list] x; y ∈ xs; xs, True.
+  Definition big_op_scope_uPred_3 (m : gmap nat nat) : uPred M :=
+    [∗ map] _ ↦ x ∈ m, True.
+  Definition big_op_scope_uPred_4 (m : gmap nat nat) : uPred M :=
+    [∗ map] x; y ∈ m; m, True.
+End base_logic_tests.
+
+Section iris_tests.
+  Context `{!invG Σ}.
+  Implicit Types P Q R : iProp Σ.
+
+  (* Test scopes for bupd and fupd *)
+  Definition use_bupd_iProp (n : nat) : iProp Σ :=
+    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.
+  Definition use_fupd_iProp (n : nat) : iProp Σ :=
+    □ |={⊤}=> ∃ m : nat , ⌜ n = 2 ⌝.
+
+  (* Test scopes inside big-ops *)
+  Definition big_op_scope_iProp_1 (xs : list nat) : iProp Σ :=
+    [∗ list] _ ↦ x ∈ xs, True.
+  Definition big_op_scope_iProp_2 (xs : list nat) : iProp Σ :=
+    [∗ list] x; y ∈ xs; xs, True.
+  Definition big_op_scope_iProp_3 (m : gmap nat nat) : iProp Σ :=
+    [∗ map] _ ↦ x ∈ m, True.
+  Definition big_op_scope_iProp_4 (m : gmap nat nat) : iProp Σ :=
+    [∗ map] x; y ∈ m; m, True.
+End iris_tests.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index f88ea6e87be6ceb6deede51eaec6331a50a3f178..f8601d2b09d2f69ae60165d367c487a5f6edea12 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -9,12 +9,6 @@ Section base_logic_tests.
   Context {M : ucmra}.
   Implicit Types P Q R : uPred M.
 
-  (* Test scopes for bupd *)
-  Definition use_bupd_uPred (n : nat) : uPred M :=
-    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.
-  Definition use_plainly_uPred (n : nat) : uPred M :=
-    ■ |==> ∃ m : nat , ⌜ n = 2 ⌝.
-
   Lemma test_random_stuff (P1 P2 P3 : nat → uPred M) :
     ⊢ ∀ (x y : nat) a b,
       x ≡ y →
@@ -61,12 +55,6 @@ Section iris_tests.
   Context `{!invG Σ, !cinvG Σ, !na_invG Σ}.
   Implicit Types P Q R : iProp Σ.
 
-  (* Test scopes for bupd and fupd *)
-  Definition use_bupd_iProp (n : nat) : iProp Σ :=
-    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.
-  Definition use_fupd_iProp (n : nat) : iProp Σ :=
-    □ |={⊤}=> ∃ m : nat , ⌜ n = 2 ⌝.
-
   Lemma test_masks  N E P Q R :
     ↑N ⊆ E →
     (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R.