From 0f2f51bafdd579d0505474cdc873a8892ba3f876 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 31 Aug 2017 00:53:42 +0200
Subject: [PATCH] The bare modality is also persistent.

---
 theories/bi/derived.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index d08f72e30..5c70f94cc 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1182,8 +1182,6 @@ Global Instance pure_persistent φ : Persistent (⌜φ⌝%I : PROP).
 Proof. by rewrite /Persistent persistently_pure. Qed.
 Global Instance emp_persistent : Persistent (emp%I : PROP).
 Proof. rewrite /Persistent. apply persistently_emp_intro. Qed.
-Global Instance persistently_persistent P : Persistent (â–¡ P).
-Proof. by rewrite /Persistent persistently_idemp. Qed.
 Global Instance and_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∧ Q).
 Proof. intros. by rewrite /Persistent persistently_and -!persistent. Qed.
@@ -1217,6 +1215,11 @@ Global Instance sep_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∗ Q).
 Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
 
+Global Instance persistently_persistent P : Persistent (â–¡ P).
+Proof. by rewrite /Persistent persistently_idemp. Qed.
+Global Instance bare_persistent P : Persistent P → Persistent (■ P).
+Proof. rewrite /bi_bare. apply _. Qed.
+
 Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
-- 
GitLab