From aae0efc9882b80f0c8c6f5bd840f1f8ccdc066cd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Mar 2018 15:25:54 +0100
Subject: [PATCH] fix a fluke

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

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 8dac672cd..33061f942 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -110,8 +110,7 @@ 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 ε = ε`, which implies together with
-       monotonicity that `ε ≼ core x`. *)
+    (* In the ordered RA model: [ε ≼ core x]. *)
     bi_mixin_persistently_emp_intro P : P ⊢ <pers> emp;
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
-- 
GitLab