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

---
 iris/algebra/proofmode_classes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index 84110cf8c..ea2908884 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -20,7 +20,7 @@ To achieve this, there are various classes with different modes:
 
 - [IsOp a b1 b2]. This class has no mode, so it can be used even to
   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
+  [IsOp (a â‹… b) a b] with cost 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 both [b1] and [b2] to be inputs.
   All usual instances should be of this class to avoid loops.
-- 
GitLab