From be38c8338d0014714dbf4243e8a97343d9b697db Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Fri, 7 May 2021 08:47:50 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 iris_staging/algebra/monotone.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris_staging/algebra/monotone.v b/iris_staging/algebra/monotone.v
index a3b21e0ef..9ca5e3cb9 100644
--- a/iris_staging/algebra/monotone.v
+++ b/iris_staging/algebra/monotone.v
@@ -15,7 +15,7 @@ Local Arguments cmra_valid _  !_ /.
 
 (* Given a preorder relation R on a type A we construct a resource algebra mra R
    and an injection principal : A -> mra R such that:
-   R x y iff principal x ≼ principal y
+   [R x y] iff [principal x ≼ principal y]
    where ≼ is the extension order of mra R resource algebra. This is exactly
    what the lemma [principal_included] shows.
 
-- 
GitLab