From 718938480a35b1af6daba8c730c85271a3ef18ce Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Aug 2022 18:19:34 +0000
Subject: [PATCH] Apply 2 suggestion(s) to 1 file(s)

---
 iris/algebra/proofmode_classes.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index 064ada07e..84110cf8c 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -22,10 +22,10 @@ To achieve this, there are various classes with different modes:
   combine/merge evars. This class has only one direct instance
   [IsOp (a â‹… b) a b] with priority 100 (so it is used last), ensuring that the
   "op" rule is used last when merging.
-- [IsOp' a b1 b2]. This class requires either [a] OR [b1] and [b2] to be inputs.
+- [IsOp' a b1 b2]. This class requires either [a] OR both [b1] and [b2] to be inputs.
   All usual instances should be of this class to avoid loops.
 - [IsOp'LR a b1 b2]. This class requires [a] to be an input and has just one
-  instance [IsOp'LR (a â‹… b) a b] with priority 0. This ensures that the "op"
+  instance [IsOp'LR (a â‹… b) a b] with cost 0. This ensures that the "op"
   rule is used first when splitting.
 *)
 Class IsOp {A : cmra} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.
-- 
GitLab