From e922a64623a835f37d678652157963d89ac53ab7 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 22 Dec 2016 13:16:40 +0100
Subject: [PATCH] Tweak core.v

---
 theories/base_logic/lib/core.v | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index ba5de9b21..fe6a0ed7d 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -7,7 +7,7 @@ Import uPred.
     in the shallow embedding. *)
 
 Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ (Q : uPred M) `(!PersistentP Q, !P -∗ Q), Q)%I.
+  (∀ `(!PersistentP Q, P ⊢ Q), Q)%I.
 
 Section core.
   Context {M : ucmraT}.
@@ -23,11 +23,18 @@ Section core.
     iIntros (HPQ). iApply HQ. unshelve iApply ("HCP" $! Q). done.
   Qed.
 
+  Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
+  Proof.
+    unfold coreP. iIntros (?? ENT) "H *". unshelve iApply ("H" $! Q). by etrans.
+  Qed.
+
+  Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
+  Proof. intros ??. rewrite !equiv_spec=>-[A B]. split; rewrite ?A // ?B //. Qed.
+
   Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
   Proof.
     iIntros (?) "HCP". unshelve iApply ("HCP" $! P). iIntros "P". done.
   Qed.
 End core.
 
-
-
+Global Opaque coreP.
\ No newline at end of file
-- 
GitLab