Fix scopes for `plainly` following !456.

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,

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.