From 8d254aadfddb8070578e5db9eed820d7a6f1111d Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 18 May 2020 15:59:50 +0200
Subject: [PATCH] Coqify the comments.

---
 theories/algebra/lib/frac_auth.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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