From bef526b4857713d7c5bf905c122fd7bd6c1858a0 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 18 May 2020 15:48:06 +0200
Subject: [PATCH] Fix notation in comments

---
 theories/algebra/lib/frac_auth.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 46d1e180d..51fb5f29b 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.
 *)
-- 
GitLab