From a3cc36e4cfc27037d7eb4b31c1851785e8c15b49 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 28 May 2020 13:20:22 +0200
Subject: [PATCH] Fix scopes of bupd and fupd

---
 tests/proofmode_iris.v | 10 ++++++++++
 theories/bi/updates.v  |  2 ++
 2 files changed, 12 insertions(+)

diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 311380d4d..4197e54c7 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 51f54aa59..ad8d6bbb0 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.
-- 
GitLab