From 48f44eb21e83a475f206afbc65fd246f36fdf618 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Mar 2018 14:42:14 +0100
Subject: [PATCH] typo

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

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index d271c2c7a..8dac672cd 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -121,7 +121,7 @@ Section bi_mixin.
 
     (* In the ordered RA model: [core x ≼ core (x ⋅ y)]. *)
     bi_mixin_persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P;
-    (* In the ordered RA model: [x â‹… core x = core x]. *)
+    (* In the ordered RA model: [x â‹… core x = x]. *)
     bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
   }.
 
-- 
GitLab