diff --git a/iris/algebra/updates.v b/iris/algebra/updates.v
index f5e61a3c1faee9b8c9eaacbb9111d313fc80abfd..57e076870430c7a695e01f87233bcb409b3355b8 100644
--- a/iris/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -52,8 +52,8 @@ Lemma cmra_update_exclusive `{!Exclusive x} y:
 Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
 
 (** Updates form a preorder. *)
-(** We set this rewrite relation's priority below the stdlib's 
-  ([impl], [iff], [eq], ...) and [≡] but above [⊑].
+(** We set this rewrite relation's cost above the stdlib's 
+  ([impl], [iff], [eq], ...) and [≡] but below [⊑].
   [eq] (at 100) < [≡] (at 150) < [cmra_update] (at 170) < [⊑] (at 200) *)
 Global Instance cmra_update_rewrite_relation :
   RewriteRelation (@cmra_update A) | 170 := {}.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index dcc1350a3265cfb0719b3637c090a132f12ad35b..1ebab781a29443aaa8f57ead534483f74dfa0369 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -235,8 +235,8 @@ Global Arguments bi_persistently {PROP} _ : simpl never, rename.
 Global Arguments bi_later {PROP} _ : simpl never, rename.
 
 Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
-(** We set this rewrite relation's priority below the stdlib's 
-  ([impl], [iff], [eq], ...) and [≡] but above [⊑].
+(** We set this rewrite relation's cost above the stdlib's 
+  ([impl], [iff], [eq], ...) and [≡] but below [⊑].
   [eq] (at 100) < [≡] (at 150) < [bi_entails _] (at 170) < [⊑] (at 200)
 *)
 Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) | 170 := {}.
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index ec0bc3199e93ab5b270bc36dfc543779dcdafa4c..77472d36c7942d204d3d4447cf8cb844798bb33e 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -759,8 +759,8 @@ Global Instance into_sep_intuitionistically `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (□ P) (□ Q1) (□ Q2) | 0.
 Proof. rewrite /IntoSep /= => ->. by rewrite intuitionistically_sep. Qed.
 (* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely.
-Also, it overlaps with `into_sep_affinely_later`, and hence has lower
-precedence. *)
+Also, it overlaps with `into_sep_affinely_later`, and hence has higher
+cost. *)
 Global Instance into_sep_affinely_trim P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (<affine> P) Q1 Q2 | 20.
 Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
index b38a3094ddd7f12ff197238fa2da99bb751af4c2..3d4ba827644d1cc9d8bb12e1d147cf0c13bf5567 100644
--- a/iris/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -244,7 +244,7 @@ Proof.
 Qed.
 
 (** AddModal *)
-(* High priority to add a [â–·] rather than a [â—‡] when [P] is timeless. *)
+(* Low cost to add a [â–·] rather than a [â—‡] when [P] is timeless. *)
 Global Instance add_modal_later_except_0 P Q :
   Timeless P → AddModal (▷ P) P (◇ Q) | 0.
 Proof.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 0767cdf874ee7121b1a258c44606e1fd68671ba7..b13aa6abd16de876b7ae3d8180703e339b191f10 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -626,7 +626,8 @@ Global Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
   FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2 := id.
 Global Instance into_wand_tc_opaque {PROP : bi} p q (R P Q : PROP) :
   IntoWand p q R P Q → IntoWand p q (tc_opaque R) P Q := id.
-(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
+(* Higher cost than [from_and_sep] so that [iCombine] does not loop.
+   FIXME: this comment is outdated and [from_and_sep] does not exist any more. *)
 Global Instance from_and_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
   FromAnd P Q1 Q2 → FromAnd (tc_opaque P) Q1 Q2 | 102 := id.
 Global Instance into_and_tc_opaque {PROP : bi} p (P Q1 Q2 : PROP) :
diff --git a/iris/proofmode/frame_instances.v b/iris/proofmode/frame_instances.v
index 3de73e25aaf3cdfbc2945b2178e9f37f1171cc98..5a221d695d7793587e41aecd1965e6ecc6ef188f 100644
--- a/iris/proofmode/frame_instances.v
+++ b/iris/proofmode/frame_instances.v
@@ -24,7 +24,7 @@ When framing [R] against itself, we leave [True] if possible (via
 [frame_here_absorbing] or [frame_affinely_here_absorbing]) since it is a weaker
 goal. Otherwise we leave [emp] via [frame_here].
 Only if all those options fail, we start decomposing [R], via instances like
-[frame_exist]. To ensure that, all other instances must have priority > 1. *)
+[frame_exist]. To ensure that, all other instances must have cost > 1. *)
 Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
 Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
 Global Instance frame_here p R : Frame p R R emp | 1.
@@ -50,7 +50,7 @@ Qed.
 Global Instance frame_here_pure a φ Q :
   FromPure a Q φ →
   TCOr (TCEq a false) (BiAffine PROP) →
-  Frame false ⌜φ⌝ Q emp | 2. (* Same prio as default. *)
+  Frame false ⌜φ⌝ Q emp | 2. (* Same cost as default. *)
 Proof.
   rewrite /FromPure /Frame => <- [->|?] /=.
   - by rewrite right_id.
@@ -69,14 +69,14 @@ Proof. by rewrite /MakeEmbed. Qed.
 
 Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
   Frame p R P Q → MakeEmbed Q Q' →
-  Frame p ⎡R⎤ ⎡P⎤ Q' | 2. (* Same prio as default. *)
+  Frame p ⎡R⎤ ⎡P⎤ Q' | 2. (* Same cost as default. *)
 Proof.
   rewrite /Frame /MakeEmbed => <- <-.
   rewrite embed_sep embed_intuitionistically_if_2 => //.
 Qed.
 Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
   Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' →
-  Frame p ⌜φ⌝ ⎡P⎤ Q' | 2. (* Same prio as default. *)
+  Frame p ⌜φ⌝ ⎡P⎤ Q' | 2. (* Same cost as default. *)
 Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
 
 Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
@@ -110,20 +110,20 @@ Qed.
 Global Instance frame_big_sepL_cons {A} p (Φ : nat → A → PROP) R Q l x l' :
   IsCons l x l' →
   Frame p R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l', Φ (S k) y) Q →
-  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2. (* Same prio as default. *)
+  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2. (* Same cost as default. *)
 Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.
 Global Instance frame_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
   IsApp l l1 l2 →
   Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
            [∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
-  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2. (* Same prio as default. *)
+  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2. (* Same cost as default. *)
 Proof. rewrite /IsApp=>->. by rewrite /Frame big_sepL_app. Qed.
 
 Global Instance frame_big_sepL2_cons {A B} p (Φ : nat → A → B → PROP)
     R Q l1 x1 l1' l2 x2 l2' :
   IsCons l1 x1 l1' → IsCons l2 x2 l2' →
   Frame p R (Φ 0 x1 x2 ∗ [∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2) Q →
-  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q. (* Default prio > 1. *)
+  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q. (* Default cost > 1. *)
 Proof. rewrite /IsCons=>-> ->. by rewrite /Frame big_sepL2_cons. Qed.
 Global Instance frame_big_sepL2_app {A B} p (Φ : nat → A → B → PROP)
     R Q l1 l1' l1'' l2 l2' l2'' :
@@ -216,7 +216,7 @@ Proof. by rewrite /MakeAffinely. Qed.
 Global Instance frame_affinely p R P Q Q' :
   TCOr (TCEq p true) (Affine R) →
   Frame p R P Q → MakeAffinely Q Q' →
-  Frame p R (<affine> P) Q'. (* Default prio > 1 *)
+  Frame p R (<affine> P) Q'. (* Default cost > 1 *)
 Proof.
   rewrite /Frame /MakeAffinely=> -[->|?] <- <- /=;
     by rewrite -{1}(affine_affinely (_ R)) affinely_sep_2.
@@ -240,7 +240,7 @@ Proof. by rewrite /MakeIntuitionistically. Qed.
 
 Global Instance frame_intuitionistically R P Q Q' :
   Frame true R P Q → MakeIntuitionistically Q Q' →
-  Frame true R (â–¡ P) Q' | 2. (* Same prio as default. *)
+  Frame true R (â–¡ P) Q' | 2. (* Same cost as default. *)
 Proof.
   rewrite /Frame /MakeIntuitionistically=> <- <- /=.
   rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
@@ -258,7 +258,7 @@ Proof. by rewrite /MakeAbsorbingly. Qed.
 
 Global Instance frame_absorbingly p R P Q Q' :
   Frame p R P Q → MakeAbsorbingly Q Q' →
-  Frame p R (<absorb> P) Q' | 2. (* Same prio as default. *)
+  Frame p R (<absorb> P) Q' | 2. (* Same cost as default. *)
 Proof.
   rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
 Qed.
@@ -276,7 +276,7 @@ Proof. by rewrite /MakePersistently. Qed.
 
 Global Instance frame_persistently R P Q Q' :
   Frame true R P Q → MakePersistently Q Q' →
-  Frame true R (<pers> P) Q' | 2. (* Same prio as default. *)
+  Frame true R (<pers> P) Q' | 2. (* Same cost as default. *)
 Proof.
   rewrite /Frame /MakePersistently=> <- <- /=.
   rewrite -persistently_and_intuitionistically_sep_l.
@@ -306,7 +306,7 @@ Proof.
 Qed.
 Global Instance frame_impl R P1 P2 Q2 :
   Persistent P1 → Absorbing P1 →
-  Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2). (* Default prio > 1 *)
+  Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2). (* Default cost > 1 *)
 Proof.
   rewrite /Frame /==> ???. apply impl_intro_l.
   rewrite {1}(persistent P1) persistently_and_intuitionistically_sep_l assoc.
@@ -318,7 +318,7 @@ Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !BiInternalEq PROP,
     !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
     p P Q (Q' : PROP') {A : ofe} (a b : A) :
   Frame p (a ≡ b) P Q → MakeEmbed Q Q' →
-  Frame p (a ≡ b) ⎡P⎤ Q'. (* Default prio > 1 *)
+  Frame p (a ≡ b) ⎡P⎤ Q'. (* Default cost > 1 *)
 Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
 
 Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
@@ -332,7 +332,7 @@ Proof. by rewrite /MakeLaterN. Qed.
 Global Instance frame_later p R R' P Q Q' :
   TCNoBackTrack (MaybeIntoLaterN true 1 R' R) →
   Frame p R P Q → MakeLaterN 1 Q Q' →
-  Frame p R' (â–· P) Q'. (* Default prio > 1 *)
+  Frame p R' (â–· P) Q'. (* Default cost > 1 *)
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
   by rewrite later_intuitionistically_if_2 later_sep.
@@ -340,7 +340,7 @@ Qed.
 Global Instance frame_laterN p n R R' P Q Q' :
   TCNoBackTrack (MaybeIntoLaterN true n R' R) →
   Frame p R P Q → MakeLaterN n Q Q' →
-  Frame p R' (â–·^n P) Q'. (* Default prio > 1 *)
+  Frame p R' (â–·^n P) Q'. (* Default cost > 1 *)
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
   by rewrite laterN_intuitionistically_if_2 laterN_sep.
@@ -360,7 +360,7 @@ Proof. by rewrite /MakeExcept0. Qed.
 
 Global Instance frame_except_0 p R P Q Q' :
   Frame p R P Q → MakeExcept0 Q Q' →
-  Frame p R (â—‡ P) Q' | 2. (* Same prio as default *)
+  Frame p R (â—‡ P) Q' | 2. (* Same cost as default *)
 Proof.
   rewrite /Frame /MakeExcept0=><- <-.
   by rewrite except_0_sep -(except_0_intro (â–¡?p R)).
diff --git a/iris_heap_lang/class_instances.v b/iris_heap_lang/class_instances.v
index 6d3dac76ddd70be58063d0655957689802c3030e..55426d9dde86397c8c0eb1d5490281362b2cba3a 100644
--- a/iris_heap_lang/class_instances.v
+++ b/iris_heap_lang/class_instances.v
@@ -134,7 +134,7 @@ Section pure_exec.
   Global Instance pure_binop op v1 v2 v' :
     PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
   Proof. solve_pure_exec. Qed.
-  (* Higher-priority instance for [EqOp]. *)
+  (* Lower-cost instance for [EqOp]. *)
   Global Instance pure_eqop v1 v2 :
     PureExec (vals_compare_safe v1 v2) 1
       (BinOp EqOp (Val v1) (Val v2))
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index b6bbbdb2d8ca99ec367a3ce8438eb6fca5ec53cf..9915457b0172f7bddab3b036778dea7d4257f637 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -250,7 +250,7 @@ Section iris_tests.
     iIntros "H H'". Fail iDestruct "H'" as ">H".
   Abort.
 
-  (** Make sure that the splitting rule for [+] gets priority over the one for
+  (** Make sure that the splitting rule for [+] gets preferred over the one for
   [S]. See issue #470. *)
   Check "test_iIntros_lc".
   Lemma test_iIntros_lc n m : £ (S n + m) -∗ £ (S n).