diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v index 25f9046b87bcb604116d77af24a6578519eb7c11..f44745158f10a3ec6e61f4380b423e38d22150ce 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')