diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 46d1e180d89c88235ceacca382f1c1050b1cdf08..51fb5f29bb288082731d3d2578c1f1c3deea9a0a 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -3,7 +3,7 @@ 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 `◯!{q} a`. Using `◯! a ≡ ◯!{1} a` is in effect the same as
+  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.
 *)