Also review Iris instances outside [frame_instances]

iris/bi/lib/fractional.v

@@ -181,7 +181,7 @@ Section fractional.
   Global Instance frame_fractional p R r Φ P q RES:
     AsFractional R Φ r → AsFractional P Φ q →
     FrameFractionalHyps p R Φ RES r q →
-    Frame p R P RES.
+    Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
   Proof.
     rewrite /Frame=>-[HR _][->?]H.
     revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].

iris/program_logic/total_weakestpre.v

@@ -284,7 +284,7 @@ Section proofmode_classes.
 
   Global Instance frame_twp p s E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →
-    Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
+    Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]) | 2.
   Proof. rewrite /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
 
   Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).

iris/program_logic/weakestpre.v

@@ -366,7 +366,7 @@ Section proofmode_classes.
 
   Global Instance frame_wp p s E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →
-    Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
+    Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}) | 2.
   Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 
   Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).

iris/proofmode/monpred.v

@@ -364,7 +364,7 @@ Qed.
 
 (* Framing. *)
 Global Instance frame_monPred_at_enter p i 𝓡 P 𝓠 :
-  FrameMonPredAt p i 𝓡 P 𝓠 → Frame p 𝓡 (P i) 𝓠.
+  FrameMonPredAt p i 𝓡 P 𝓠 → Frame p 𝓡 (P i) 𝓠 | 2.
 Proof. intros. done. Qed.
 Global Instance frame_monPred_at_here p P i j :
   IsBiIndexRel i j → FrameMonPredAt p j (P i) P emp | 0.

iris_heap_lang/derived_laws.v

@@ -73,7 +73,7 @@ Qed.
 
 Global Instance array_cons_frame l dq v vs R Q :
   Frame false R (l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs) Q →
-  Frame false R (l ↦∗{dq} (v :: vs)) Q.
+  Frame false R (l ↦∗{dq} (v :: vs)) Q | 2.
 Proof. by rewrite /Frame array_cons. Qed.
 
 Lemma update_array l dq vs off v :