From 56056f6620740ab70f2ccd58b882a7cb47faff8a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Mar 2018 10:58:45 +0100
Subject: [PATCH] =?UTF-8?q?pers-emp=20actually=20just=20needs=20`core=20?=
 =?UTF-8?q?=CE=B5=20=3D=20=CE=B5`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/interface.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 4bc097288..2b595d700 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -110,7 +110,8 @@ Section bi_mixin.
     (* In the ordered RA model: `core` is idempotent *)
     bi_mixin_persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P;
 
-    (* In the ordered RA model: `ε ≼ core x` *)
+    (* In the ordered RA model: `core ε = ε`, which implies together with
+       monotonicity that `ε ≼ core x`. *)
     bi_mixin_persistently_emp_intro P : P ⊢ <pers> emp;
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
-- 
GitLab