From 38f2b14cbf022ad2b5237714df388e47ef850d3a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 May 2023 23:08:12 +0200
Subject: [PATCH] fix outdated comment

Thanks, Johannes!
---
 iris/algebra/dfrac.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index 25f9046b8..f44745158 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -90,7 +90,7 @@ Section dfrac.
     end.
 
   (** When elements are combined, ownership is added together and knowledge of
-     discarded fractions is combined with the max operation. *)
+     discarded fractions is preserved. *)
   Local Instance dfrac_op_instance : Op dfrac := λ dq dp,
     match dq, dp with
     | DfracOwn q, DfracOwn q' => DfracOwn (q + q')
-- 
GitLab