diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index a31bdb83f1a1f2cd3b8f5f52ab3703c9f8d989eb..44966f828664a31297d532b0c7ce1431aeb20cd4 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -9,9 +9,7 @@ difference:
   if we have the authoritative element we can always increase its fraction
   and allocate a new fragment.
 
-  <<<
   ✓ (a ⋅ b) → ●U_p a ~~> ●U_(p + q) (a ⋅ b) ⋅ ◯U_q b
-  >>>
 
 - We no longer have the [â—¯U{1} a] is the exclusive fragmental element (cf.
   [frac_auth_frag_validN_op_1_l]).
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 2e7b93e3dc9b36881c8477e2431bef2e07d1ef27..32f3eb0ea0c29c48cb3715aa9a58751430a5123b 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 Import bi.
 
 (* FIXME(Coq #6294): needs new unification *)
-(** The lemma [from_assumption_exact is not an instance, but defined using
+(** The lemma [from_assumption_exact] is not an instance, but defined using
 [notypeclasses refine] through [Hint Extern] to enable the better unification
 algorithm. We use [shelve] to avoid the creation of unshelved goals for evars
 by [refine], which otherwise causes TC search to fail. Such unshelved goals are