diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 4197e54c731958b6d6e0f3aef48fea8a471dcdd6..416707464aa0083706188a93dc82f3f452f646c8 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -9,6 +9,8 @@ Section base_logic_tests.
   (* 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,
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index a5b5af0210bf293e7b5abf9ac2c7cf67c656cf2c..b81fe05d1a1c468757758a2072dffc5082044b27 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -3,6 +3,7 @@ From iris.algebra Require Import monoid.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 Class Plainly (A : Type) := plainly : A → A.
+Arguments plainly {A}%type_scope {_} _%I.
 Hint Mode Plainly ! : typeclass_instances.
 Instance: Params (@plainly) 2 := {}.
 Notation "â–  P" := (plainly P) : bi_scope.