diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index 84110cf8c1cd23e2b86efbfa10c87c999f101be0..ea29088847fff5cf7610c2670b50b39a3f97293c 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.