diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index 26065b4ec0dea4e215397f765bf5728a13a471e8..2c9d71237abddaea9a4f1dc063af43c20845d587 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -177,17 +177,6 @@ Proof.
   rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
 Qed.
 
-Global Instance make_persistently_emp : @KnownMakePersistently PROP emp True.
-Proof.
-  by rewrite /KnownMakePersistently /MakePersistently
-     -persistently_True_emp persistently_pure.
-Qed.
-Global Instance make_persistently_True : @KnownMakePersistently PROP True True.
-Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
-Global Instance make_persistently_default P :
-  MakePersistently P (<pers> P) | 100.
-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 cost as default. *)
diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v
index 3fef78dbeff1d87bc30e43a03079f5f0545b190f..bb638daf7d86c7475e0e4c41a90738bf45aa779a 100644
--- a/iris/proofmode/class_instances_make.v
+++ b/iris/proofmode/class_instances_make.v
@@ -85,10 +85,14 @@ Proof. by rewrite /MakeOr. Qed.
   to avoid [emp] in goals involving affine BIs, we give [make_affinely_affine]
   a lower cost than [make_affinely_True].
 - [make_affinely_default] adds the modality. This is the default instance since
-  it can always be used, and thus has the highest cost. *)
+  it can always be used, and thus has the highest cost.
+  (For this last point, the cost of the [KnownMakeAffinely] instances does not
+  actually matter, since this is a [MakeAffinely] instance, i.e. an instance of
+  a different class. What really matters is that the [known_make_affinely]
+  instance has a lower cost than [make_affinely_default].) *)
 
 Global Instance make_affinely_affine P :
-  QuickAffine P → MakeAffinely P P | 0.
+  QuickAffine P → KnownMakeAffinely P P | 0.
 Proof. apply affine_affinely. Qed.
 Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 1.
 Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
@@ -105,10 +109,14 @@ Proof. by rewrite /MakeAffinely. Qed.
   it does not really matter since goals in affine BIs typically do not contain
   occurrences of [emp] to start with.
 - [make_absorbingly_default] adds the modality. This is the default instance
-  since it can always be used, and thus has the highest cost. *)
+  since it can always be used, and thus has the highest cost.
+  (For this last point, the cost of the [KnownMakeAbsorbingly] instances does not
+  actually matter, since this is a [MakeAbsorbingly] instance, i.e. an instance of
+  a different class. What really matters is that the [known_make_absorbingly]
+  instance has a lower cost than [make_absorbingly_default].) *)
 
 Global Instance make_absorbingly_absorbing P :
-  QuickAbsorbing P → MakeAbsorbingly P P | 0.
+  QuickAbsorbing P → KnownMakeAbsorbingly P P | 0.
 Proof. apply absorbing_absorbingly. Qed.
 Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 1.
 Proof.
@@ -117,6 +125,20 @@ Qed.
 Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
 Proof. by rewrite /MakeAbsorbingly. Qed.
 
+(** Persistently *)
+Global Instance make_persistently_emp :
+  @KnownMakePersistently PROP emp True | 0.
+Proof.
+  by rewrite /KnownMakePersistently /MakePersistently
+     -persistently_True_emp persistently_pure.
+Qed.
+Global Instance make_persistently_True :
+  @KnownMakePersistently PROP True True | 0.
+Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
+Global Instance make_persistently_default P :
+  MakePersistently P (<pers> P) | 100.
+Proof. by rewrite /MakePersistently. Qed.
+
 (** Intuitionistically *)
 Global Instance make_intuitionistically_emp :
   @KnownMakeIntuitionistically PROP emp emp | 0.
@@ -124,8 +146,17 @@ Proof.
   by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
     intuitionistically_emp.
 Qed.
+(** For affine BIs, we would prefer [â–¡ True] to become [True] rather than [emp],
+so we have this instance with lower cost than the next. *)
+Global Instance make_intuitionistically_True_affine :
+  BiAffine PROP →
+  @KnownMakeIntuitionistically PROP True True | 0.
+Proof.
+  intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
+    intuitionistically_True_emp True_emp //.
+Qed.
 Global Instance make_intuitionistically_True :
-  @KnownMakeIntuitionistically PROP True emp | 0.
+  @KnownMakeIntuitionistically PROP True emp | 1.
 Proof.
   by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
     intuitionistically_True_emp.
diff --git a/iris/proofmode/classes_make.v b/iris/proofmode/classes_make.v
index 7d0bda7a2248c1f0784c50b5781139d482cc9331..4af72163fd943e245b8abd70d85bfb8b093b4eae 100644
--- a/iris/proofmode/classes_make.v
+++ b/iris/proofmode/classes_make.v
@@ -35,7 +35,10 @@ evar, then [MakeX] will not instantiate it arbitrarily.
 The reason for this is that if given an evar, these classes would typically
 try to instantiate this evar with some arbitrary logical constructs such as
 [emp] or [True]. Therefore, we use a [Hint Mode] to disable all the instances
-that would have this behavior. *)
+that would have this behavior.
+
+In practice this means that usually only the default instance should use [MakeX],
+and most specialized instances should use [KnownMakeX]. *)
 From iris.bi Require Export bi.
 From iris.prelude Require Import options.
 
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 749eb5b9724b4f32b92e656613d6ea16ea9c9c2d..57992ccc987e921af097c8a1edf82395f3d2dc73 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -503,9 +503,9 @@ No applicable tactic.
 1 goal
   
   PROP : bi
-  H : BiAffine PROP
+  BiAffine0 : BiAffine PROP
   P, Q : PROP
-  H0 : Laterable Q
+  H : Laterable Q
   ============================
   "HP" : â–· P
   "HQ" : Q
@@ -534,6 +534,17 @@ No applicable tactic.
   "H" : ⌜φ⌝ -∗ P
   --------------------------------------∗
   ⌜φ⌝ -∗ P
+"test_iFrame_not_add_emp_for_intuitionistically"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  P : PROP
+  ============================
+  "H" : P
+  --------------------------------------â–¡
+  ∃ _ : nat, True
 "elim_mod_accessor"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 3fe9aed5fe185a7771b32a1214ca2e7e5d19fffa..2d08f83fe9d7ee65a1cba3df9fb178f75479ad52 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1261,7 +1261,7 @@ Proof.
   iIntros "[P _]". done.
 Qed.
 
-Lemma test_iModIntro_make_laterable `{BiAffine PROP} (P Q : PROP) :
+Lemma test_iModIntro_make_laterable `{!BiAffine PROP} (P Q : PROP) :
   Laterable Q →
   P -∗ Q -∗ make_laterable (▷ P ∗ Q).
 Proof.
@@ -1284,6 +1284,13 @@ Proof.
   iIntros (Hφ) "H". iRevert (Hφ). Show. done.
 Qed.
 
+(* Check that when framing things under the â–¡ modality, we do not add [emp] in
+affine BIs. *)
+Check "test_iFrame_not_add_emp_for_intuitionistically".
+Lemma test_iFrame_not_add_emp_for_intuitionistically `{!BiAffine PROP} (P : PROP) :
+  □ P -∗ ∃ _ : nat, □ P.
+Proof. iIntros "#H". iFrame "H". Show. by iExists 0. Qed.
+
 End tests.
 
 Section parsing_tests.