From 7458fa675a935384ffe607c52adbe54e4ec0fb96 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" 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