From 7458fa675a935384ffe607c52adbe54e4ec0fb96 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 28 May 2020 15:01:43 +0200
Subject: [PATCH] Fix scopes for `plainly` following !456.

---
 tests/proofmode_iris.v | 2 ++
 theories/bi/plainly.v  | 1 +
 2 files changed, 3 insertions(+)

diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 4197e54c7..416707464 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 a5b5af021..b81fe05d1 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.
-- 
GitLab