diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 51fb5f29bb288082731d3d2578c1f1c3deea9a0a..324de2eacc3627aa32348edf73874e1b519117c3 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -2,9 +2,9 @@ From iris.algebra Require Export frac auth updates local_updates.
 From iris.algebra Require Import proofmode_classes.
 
 (** Authoritative CMRA where the NON-authoritative parts can be fractional.
-  This CMRA allows the original non-authoritative element `â—¯ a` to be split into
-  fractional parts `◯F{q} a`. Using `◯F a ≡ ◯F{1} a` is in effect the same as
-  using the original `â—¯ a`. Currently, however, this CMRA hides the ability to
+  This CMRA allows the original non-authoritative element [â—¯ a] to be split into
+  fractional parts [◯F{q} a]. Using [◯F a ≡ ◯F{1} a] is in effect the same as
+  using the original [â—¯ a]. Currently, however, this CMRA hides the ability to
   split the authoritative part into fractions.
 *)