From 6db3649fbadc1cdd76711ba5cb4a19db903f4331 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Wed, 28 Jul 2021 09:41:07 +0000
Subject: [PATCH] improve comments

---
 iris/bi/interface.v | 4 ++--
 iris/bi/plainly.v   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 2e80cf981..ef82d1380 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -104,8 +104,8 @@ Section bi_mixin.
     (* The laws of a "frame" (https://ncatlab.org/nlab/show/frame, not to be
     confused with separation logic terminology): commuting with finite
     conjunction and infinite disjunction.
-    The null-ary case, [True ⊢ <pers> True], is derivable from the other laws
-    ([persistently_True]). *)
+    The null-ary case, [persistently_True : True ⊢ <pers> True], is derivable from the
+    other laws. *)
     bi_mixin_persistently_and_2 (P Q : PROP) :
       ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q);
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index c050f38c8..dbc5cde46 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -25,7 +25,7 @@ Record BiPlainlyMixin (PROP : bi) `(Plainly PROP) := {
 
   (* The following law and [persistently_impl_plainly] below are very similar,
      and indeed they hold not just for persistently and plainly, but for any
-     modality defined as `M P n x := ∀ y, R x y → P n y`. *)
+     modality defined as [M P n x := ∀ y, R x y → P n y]. *)
   bi_plainly_mixin_plainly_impl_plainly (P Q : PROP) :
     (■ P → ■ Q) ⊢ ■ (■ P → Q);
 
-- 
GitLab