Merge branch 'bfupd-scopes' into 'master'

Fix scopes of bupd and fupd

See merge request iris/iris!456

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.

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.