From d080eb82e222edeb1c0bce18678b731404e2a006 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 May 2022 09:54:28 +0200
Subject: [PATCH] bring back the verbatim

---
 iris/algebra/lib/ufrac_auth.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index 44966f828..12311d84c 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -9,7 +9,9 @@ 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
+<<
+✓ (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]).
-- 
GitLab