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 0d1c96a3a02f43e9f777bec66c71c33c9e7c9a79..f8601d2b09d2f69ae60165d367c487a5f6edea12 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -9,22 +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 ⌝.
-
-  (* Test scopes inside big-ops *)
-  Definition big_op_scope_1 (xs : list nat) : uPred M :=
-    [∗ list] _ ↦ x ∈ xs, True.
-  Definition big_op_scope_2 (xs : list nat) : uPred M :=
-    [∗ list] x; y ∈ xs; xs, True.
-  Definition big_op_scope_3 (m : gmap nat nat) : uPred M :=
-    [∗ map] _ ↦ x ∈ m, True.
-  Definition big_op_scope_4 (m : gmap nat nat) : uPred M :=
-    [∗ map] x; y ∈ m; m, True.
-
   Lemma test_random_stuff (P1 P2 P3 : nat → uPred M) :
     ⊢ ∀ (x y : nat) a b,
       x ≡ y →
@@ -71,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.