diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 311380d4dcaafb514acd0ae0b9ca1dd0dc287285..4197e54c731958b6d6e0f3aef48fea8a471dcdd6 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -6,6 +6,10 @@ Section base_logic_tests.
   Context {M : ucmraT}.
   Implicit Types P Q R : uPred M.
 
+  (* Test scopes for bupd *)
+  Definition use_bupd_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 →
@@ -52,6 +56,12 @@ 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.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 51f54aa594416bc12dfbfd5497455cb50f101db5..ad8d6bbb0459dedf5fb71bdbfbeb85e4a4367e88 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -7,6 +7,7 @@ bundle these operational type classes with the laws. *)
 Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
 Instance : Params (@bupd) 2 := {}.
 Hint Mode BUpd ! : typeclass_instances.
+Arguments bupd {_}%type_scope {_} _%bi_scope.
 
 Notation "|==> Q" := (bupd Q) : bi_scope.
 Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
@@ -15,6 +16,7 @@ Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
 Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
 Instance: Params (@fupd) 4 := {}.
 Hint Mode FUpd ! : typeclass_instances.
+Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
 
 Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
 Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I : bi_scope.