diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 2e80cf981473baa84125dcb4f79125849c3a1229..ef82d1380c51ab2e0c0e7d8e543874d441a5ffe2 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 c050f38c8a794b2b749d53c901b64aaece384beb..dbc5cde46b4cb31ad0ef074206a44570096ccbba 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);