diff --git a/_CoqProject b/_CoqProject
index fbd492264bbf37a2bae7ebd227db0580c39141f7..198cf2a91544ca0b088c43b9b197aa01e681f6cf 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -134,6 +134,7 @@ iris/proofmode/sel_patterns.v
 iris/proofmode/tactics.v
 iris/proofmode/notation.v
 iris/proofmode/classes.v
+iris/proofmode/classes_make.v
 iris/proofmode/class_instances.v
 iris/proofmode/class_instances_later.v
 iris/proofmode/class_instances_updates.v
@@ -141,6 +142,7 @@ iris/proofmode/class_instances_embedding.v
 iris/proofmode/class_instances_plainly.v
 iris/proofmode/class_instances_internal_eq.v
 iris/proofmode/class_instances_frame.v
+iris/proofmode/class_instances_make.v
 iris/proofmode/monpred.v
 iris/proofmode/modalities.v
 iris/proofmode/modality_instances.v
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 9b48116c8ac43250d1f60c7b2889a1b782dca1bb..935a206e703ec2755a4f4fcd92bb3b09efff620a 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export bi.
-From iris.proofmode Require Import classes class_instances.
+From iris.proofmode Require Import classes classes_make.
 From iris.prelude Require Import options.
 
 Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 77472d36c7942d204d3d4447cf8cb844798bb33e..46f933bb3a23f11cd4c497cc1780ea79b18bbef4 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -1,5 +1,4 @@
-From stdpp Require Import nat_cancel.
-From iris.bi Require Import bi telescopes.
+From iris.bi Require Import telescopes.
 From iris.proofmode Require Import base modality_instances classes.
 From iris.proofmode Require Import ltac_tactics.
 From iris.prelude Require Import options.
diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index 5a221d695d7793587e41aecd1965e6ecc6ef188f..caf26c09bd913c3ef329724b82a05895780beff3 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -1,6 +1,5 @@
-From stdpp Require Import nat_cancel.
-From iris.bi Require Import bi telescopes.
-From iris.proofmode Require Import classes.
+From iris.bi Require Import telescopes.
+From iris.proofmode Require Import classes classes_make.
 From iris.prelude Require Import options.
 Import bi.
 
@@ -15,12 +14,11 @@ https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/450 for some modalities,
 but that makes framing less predictable and might have some performance impact.
 Hence, we only perform such cleanup for [True] and [emp]. *)
 
-Section bi.
+Section class_instances_frame.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
-(* Frame *)
-(**
-When framing [R] against itself, we leave [True] if possible (via
+
+(** 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
@@ -57,16 +55,6 @@ Proof.
   - by rewrite right_id -affinely_affinely_if affine_affinely.
 Qed.
 
-Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
-  KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
-Proof. apply embed_pure. Qed.
-Global Instance make_embed_emp `{BiEmbedEmp PROP PROP'} :
-  KnownMakeEmbed (PROP:=PROP) emp emp.
-Proof. apply embed_emp. Qed.
-Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
-  MakeEmbed P ⎡P⎤ | 100.
-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 cost as default. *)
@@ -79,17 +67,6 @@ Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
   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.
-Proof. apply left_id, _. Qed.
-Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
-Proof. apply right_id, _. Qed.
-Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P.
-Proof. intros. apply True_sep, _. Qed.
-Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
-Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
-Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
-Proof. by rewrite /MakeSep. Qed.
-
 Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
   Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress → MakeSep Q1 Q2 Q' →
   Frame true R (P1 ∗ P2) Q' | 9.
@@ -138,17 +115,6 @@ Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R
   Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
 Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
 
-Global Instance make_and_true_l P : KnownLMakeAnd True P P.
-Proof. apply left_id, _. Qed.
-Global Instance make_and_true_r P : KnownRMakeAnd P True P.
-Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
-Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P.
-Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed.
-Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P.
-Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
-Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
-Proof. by rewrite /MakeAnd. Qed.
-
 Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
   MaybeFrame p R P1 Q1 progress1 →
   MaybeFrame p R P2 Q2 progress2 →
@@ -160,19 +126,8 @@ Proof.
   apply and_intro; [rewrite and_elim_l|rewrite and_elim_r]; done.
 Qed.
 
-Global Instance make_or_true_l P : KnownLMakeOr True P True.
-Proof. apply left_absorb, _. Qed.
-Global Instance make_or_true_r P : KnownRMakeOr P True True.
-Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.
-Global Instance make_or_emp_l P : Affine P → KnownLMakeOr emp P emp.
-Proof. intros. by rewrite /KnownLMakeOr /MakeOr emp_or. Qed.
-Global Instance make_or_emp_r P : Affine P → KnownRMakeOr P emp emp.
-Proof. intros. by rewrite /KnownRMakeOr /MakeOr or_emp. Qed.
-Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
-Proof. by rewrite /MakeOr. Qed.
-
-(* We could in principle write the instance [frame_or_spatial] by a bunch of
-instances, i.e. (omitting the parameter [p = false]):
+(** We could in principle write the instance [frame_or_spatial] by a bunch of
+instances (omitting the parameter [p = false]):
 
   Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2)
   Frame R P1 True → Frame R (P1 ∨ P2) P2
@@ -184,6 +139,7 @@ appears at most once.
 
 If Coq would memorize the results of type class resolution, the solution with
 multiple instances would be preferred (and more Prolog-like). *)
+
 Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
   MaybeFrame false R P1 Q1 progress1 → MaybeFrame false R P2 Q2 progress2 →
   TCOr (TCEq (progress1 && progress2) true) (TCOr
@@ -206,13 +162,6 @@ Proof.
   by rewrite assoc (comm _ P1) -assoc wand_elim_r.
 Qed.
 
-Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0.
-Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed.
-Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
-Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
-Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
-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' →
@@ -222,22 +171,6 @@ Proof.
     by rewrite -{1}(affine_affinely (_ R)) affinely_sep_2.
 Qed.
 
-Global Instance make_intuitionistically_emp :
-  @KnownMakeIntuitionistically PROP emp emp | 0.
-Proof.
-  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
-    intuitionistically_emp.
-Qed.
-Global Instance make_intuitionistically_True :
-  @KnownMakeIntuitionistically PROP True emp | 0.
-Proof.
-  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
-    intuitionistically_True_emp.
-Qed.
-Global Instance make_intuitionistically_default P :
-  MakeIntuitionistically P (â–¡ P) | 100.
-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 cost as default. *)
@@ -246,16 +179,6 @@ Proof.
   rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
 Qed.
 
-Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
-Proof.
-  by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
-     -absorbingly_emp_True.
-Qed.
-Global Instance make_absorbingly_True : @KnownMakeAbsorbingly PROP True True | 0.
-Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbingly_pure. Qed.
-Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
-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 cost as default. *)
@@ -321,14 +244,6 @@ Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !BiInternalEq PROP,
   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.
-Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
-Global Instance make_laterN_emp `{!BiAffine PROP} n :
-  @KnownMakeLaterN PROP n emp emp | 0.
-Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
-Global Instance make_laterN_default n P : MakeLaterN n P (â–·^n P) | 100.
-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' →
@@ -353,11 +268,6 @@ Global Instance frame_fupd `{BiFUpd PROP} p E1 E2 R P Q :
   Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 2.
 Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
 
-Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
-Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.
-Global Instance make_except_0_default P : MakeExcept0 P (â—‡ P) | 100.
-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 cost as default *)
@@ -365,4 +275,4 @@ Proof.
   rewrite /Frame /MakeExcept0=><- <-.
   by rewrite except_0_sep -(except_0_intro (â–¡?p R)).
 Qed.
-End bi.
+End class_instances_frame.
diff --git a/iris/proofmode/class_instances_internal_eq.v b/iris/proofmode/class_instances_internal_eq.v
index 6bfde426cd9114824c07a7fe44de27d903932510..c37e4a6abd8cdfb827e4cd6851fd0bee97abdcd1 100644
--- a/iris/proofmode/class_instances_internal_eq.v
+++ b/iris/proofmode/class_instances_internal_eq.v
@@ -1,5 +1,4 @@
 From stdpp Require Import nat_cancel.
-From iris.bi Require Import bi.
 From iris.proofmode Require Import modality_instances classes.
 From iris.prelude Require Import options.
 Import bi.
@@ -25,7 +24,7 @@ Global Instance into_laterN_Next {A : ofe} only_head n n' (x y : A) :
   NatCancel n 1 n' 0 →
   IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
 Proof.
-  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel Nat.add_0_r.
+  rewrite /IntoLaterN /MaybeIntoLaterN /NatCancel Nat.add_0_r.
   move=> <-. rewrite later_equivI. by rewrite Nat.add_comm /= -laterN_intro.
 Qed.
 
diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
index 2fc06fa62d672b97106395460bf509a6c6886536..09d0cf4d01eae8be370a78814894d0ad361bf69c 100644
--- a/iris/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -1,6 +1,5 @@
 From stdpp Require Import nat_cancel.
-From iris.bi Require Import bi.
-From iris.proofmode Require Import modality_instances classes.
+From iris.proofmode Require Import classes classes_make modality_instances.
 From iris.prelude Require Import options.
 Import bi.
 
diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v
new file mode 100644
index 0000000000000000000000000000000000000000..844b796adb983fafe4136e5d7e8dc0f30fd77d63
--- /dev/null
+++ b/iris/proofmode/class_instances_make.v
@@ -0,0 +1,97 @@
+From iris.proofmode Require Export classes_make.
+From iris.prelude Require Import options.
+Import bi.
+
+Section class_instances_make.
+Context {PROP : bi}.
+Implicit Types P Q R : PROP.
+
+Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
+  KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
+Proof. apply embed_pure. Qed.
+Global Instance make_embed_emp `{BiEmbedEmp PROP PROP'} :
+  KnownMakeEmbed (PROP:=PROP) emp emp.
+Proof. apply embed_emp. Qed.
+Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
+  MakeEmbed P ⎡P⎤ | 100.
+Proof. by rewrite /MakeEmbed. Qed.
+
+Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
+Proof. apply left_id, _. Qed.
+Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
+Proof. apply right_id, _. Qed.
+Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P.
+Proof. intros. apply True_sep, _. Qed.
+Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
+Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
+Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
+Proof. by rewrite /MakeSep. Qed.
+
+Global Instance make_and_true_l P : KnownLMakeAnd True P P.
+Proof. apply left_id, _. Qed.
+Global Instance make_and_true_r P : KnownRMakeAnd P True P.
+Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
+Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P.
+Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed.
+Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P.
+Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
+Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
+Proof. by rewrite /MakeAnd. Qed.
+
+Global Instance make_or_true_l P : KnownLMakeOr True P True.
+Proof. apply left_absorb, _. Qed.
+Global Instance make_or_true_r P : KnownRMakeOr P True True.
+Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.
+Global Instance make_or_emp_l P : Affine P → KnownLMakeOr emp P emp.
+Proof. intros. by rewrite /KnownLMakeOr /MakeOr emp_or. Qed.
+Global Instance make_or_emp_r P : Affine P → KnownRMakeOr P emp emp.
+Proof. intros. by rewrite /KnownRMakeOr /MakeOr or_emp. Qed.
+Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
+Proof. by rewrite /MakeOr. Qed.
+
+Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0.
+Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed.
+Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
+Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
+Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
+Proof. by rewrite /MakeAffinely. Qed.
+
+Global Instance make_intuitionistically_emp :
+  @KnownMakeIntuitionistically PROP emp emp | 0.
+Proof.
+  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
+    intuitionistically_emp.
+Qed.
+Global Instance make_intuitionistically_True :
+  @KnownMakeIntuitionistically PROP True emp | 0.
+Proof.
+  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
+    intuitionistically_True_emp.
+Qed.
+Global Instance make_intuitionistically_default P :
+  MakeIntuitionistically P (â–¡ P) | 100.
+Proof. by rewrite /MakeIntuitionistically. Qed.
+
+Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
+Proof.
+  by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
+     -absorbingly_emp_True.
+Qed.
+Global Instance make_absorbingly_True : @KnownMakeAbsorbingly PROP True True | 0.
+Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbingly_pure. Qed.
+Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
+Proof. by rewrite /MakeAbsorbingly. Qed.
+
+Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
+Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
+Global Instance make_laterN_emp `{!BiAffine PROP} n :
+  @KnownMakeLaterN PROP n emp emp | 0.
+Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
+Global Instance make_laterN_default n P : MakeLaterN n P (â–·^n P) | 100.
+Proof. by rewrite /MakeLaterN. Qed.
+
+Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
+Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.
+Global Instance make_except_0_default P : MakeExcept0 P (â—‡ P) | 100.
+Proof. by rewrite /MakeExcept0. Qed.
+End class_instances_make.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index e5c8570f1127d47ad37f2eff7ac08086f93fc8ee..29a40387cfbe78074432952c74d9850db032845d 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -321,113 +321,6 @@ Global Instance maybe_frame_default {PROP : bi} (R P : PROP) :
   TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.
 Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
 
-(* For each of the [MakeXxxx] class, there is a [KnownMakeXxxx]
-   variant, that only succeeds if the parameter(s) is not an evar. In
-   the case the parameter(s) is an evar, then [MakeXxxx] will not
-   instantiate it arbitrarily.
-
-   The reason for this is that if given an evar, these typeclasses
-   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. *)
-Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
-  make_embed : ⎡P⎤ ⊣⊢ Q.
-Global Arguments MakeEmbed {_ _ _} _%I _%I.
-Global Hint Mode MakeEmbed + + + - - : typeclass_instances.
-Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
-  known_make_embed :> MakeEmbed P Q.
-Global Arguments KnownMakeEmbed {_ _ _} _%I _%I.
-Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
-
-Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
-Global Arguments MakeSep {_} _%I _%I _%I.
-Global Hint Mode MakeSep + - - - : typeclass_instances.
-Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
-  knownl_make_sep :> MakeSep P Q PQ.
-Global Arguments KnownLMakeSep {_} _%I _%I _%I.
-Global Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
-Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
-  knownr_make_sep :> MakeSep P Q PQ.
-Global Arguments KnownRMakeSep {_} _%I _%I _%I.
-Global Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
-
-Class MakeAnd {PROP : bi} (P Q PQ : PROP) :=  make_and_l : P ∧ Q ⊣⊢ PQ.
-Global Arguments MakeAnd {_} _%I _%I _%I.
-Global Hint Mode MakeAnd + - - - : typeclass_instances.
-Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
-  knownl_make_and :> MakeAnd P Q PQ.
-Global Arguments KnownLMakeAnd {_} _%I _%I _%I.
-Global Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
-Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
-  knownr_make_and :> MakeAnd P Q PQ.
-Global Arguments KnownRMakeAnd {_} _%I _%I _%I.
-Global Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
-
-Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
-Global Arguments MakeOr {_} _%I _%I _%I.
-Global Hint Mode MakeOr + - - - : typeclass_instances.
-Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
-  knownl_make_or :> MakeOr P Q PQ.
-Global Arguments KnownLMakeOr {_} _%I _%I _%I.
-Global Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
-Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
-Global Arguments KnownRMakeOr {_} _%I _%I _%I.
-Global Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
-
-Class MakeAffinely {PROP : bi} (P Q : PROP) :=
-  make_affinely : <affine> P ⊣⊢ Q.
-Global Arguments MakeAffinely {_} _%I _%I.
-Global Hint Mode MakeAffinely + - - : typeclass_instances.
-Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
-  known_make_affinely :> MakeAffinely P Q.
-Global Arguments KnownMakeAffinely {_} _%I _%I.
-Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
-
-Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
-  make_intuitionistically : □ P ⊣⊢ Q.
-Global Arguments MakeIntuitionistically {_} _%I _%I.
-Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
-Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
-  known_make_intuitionistically :> MakeIntuitionistically P Q.
-Global Arguments KnownMakeIntuitionistically {_} _%I _%I.
-Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
-
-Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
-  make_absorbingly : <absorb> P ⊣⊢ Q.
-Global Arguments MakeAbsorbingly {_} _%I _%I.
-Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
-Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
-  known_make_absorbingly :> MakeAbsorbingly P Q.
-Global Arguments KnownMakeAbsorbingly {_} _%I _%I.
-Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
-
-Class MakePersistently {PROP : bi} (P Q : PROP) :=
-  make_persistently : <pers> P ⊣⊢ Q.
-Global Arguments MakePersistently {_} _%I _%I.
-Global Hint Mode MakePersistently + - - : typeclass_instances.
-Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
-  known_make_persistently :> MakePersistently P Q.
-Global Arguments KnownMakePersistently {_} _%I _%I.
-Global Hint Mode KnownMakePersistently + ! - : typeclass_instances.
-
-Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
-  make_laterN : ▷^n P ⊣⊢ lP.
-Global Arguments MakeLaterN {_} _%nat _%I _%I.
-Global Hint Mode MakeLaterN + + - - : typeclass_instances.
-Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
-  known_make_laterN :> MakeLaterN n P lP.
-Global Arguments KnownMakeLaterN {_} _%nat _%I _%I.
-Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
-
-Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
-  make_except_0 : ◇ P ⊣⊢ Q.
-Global Arguments MakeExcept0 {_} _%I _%I.
-Global Hint Mode MakeExcept0 + - - : typeclass_instances.
-Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
-  known_make_except_0 :> MakeExcept0 P Q.
-Global Arguments KnownMakeExcept0 {_} _%I _%I.
-Global Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
-
 Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
 Global Arguments IntoExcept0 {_} _%I _%I : simpl never.
 Global Arguments into_except_0 {_} _%I _%I {_}.
diff --git a/iris/proofmode/classes_make.v b/iris/proofmode/classes_make.v
new file mode 100644
index 0000000000000000000000000000000000000000..8d629ee395cf6adfce41914ad2e74de8ec1c6e33
--- /dev/null
+++ b/iris/proofmode/classes_make.v
@@ -0,0 +1,110 @@
+From iris.bi Require Export bi.
+From iris.prelude Require Import options.
+
+(* For each of the [MakeXxxx] class, there is a [KnownMakeXxxx]
+   variant, that only succeeds if the parameter(s) is not an evar. In
+   the case the parameter(s) is an evar, then [MakeXxxx] will not
+   instantiate it arbitrarily.
+
+   The reason for this is that if given an evar, these typeclasses
+   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. *)
+
+Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
+  make_embed : ⎡P⎤ ⊣⊢ Q.
+Global Arguments MakeEmbed {_ _ _} _%I _%I.
+Global Hint Mode MakeEmbed + + + - - : typeclass_instances.
+Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
+  known_make_embed :> MakeEmbed P Q.
+Global Arguments KnownMakeEmbed {_ _ _} _%I _%I.
+Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
+
+Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
+Global Arguments MakeSep {_} _%I _%I _%I.
+Global Hint Mode MakeSep + - - - : typeclass_instances.
+Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
+  knownl_make_sep :> MakeSep P Q PQ.
+Global Arguments KnownLMakeSep {_} _%I _%I _%I.
+Global Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
+Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
+  knownr_make_sep :> MakeSep P Q PQ.
+Global Arguments KnownRMakeSep {_} _%I _%I _%I.
+Global Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
+
+Class MakeAnd {PROP : bi} (P Q PQ : PROP) :=  make_and_l : P ∧ Q ⊣⊢ PQ.
+Global Arguments MakeAnd {_} _%I _%I _%I.
+Global Hint Mode MakeAnd + - - - : typeclass_instances.
+Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
+  knownl_make_and :> MakeAnd P Q PQ.
+Global Arguments KnownLMakeAnd {_} _%I _%I _%I.
+Global Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
+Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
+  knownr_make_and :> MakeAnd P Q PQ.
+Global Arguments KnownRMakeAnd {_} _%I _%I _%I.
+Global Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
+
+Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
+Global Arguments MakeOr {_} _%I _%I _%I.
+Global Hint Mode MakeOr + - - - : typeclass_instances.
+Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
+  knownl_make_or :> MakeOr P Q PQ.
+Global Arguments KnownLMakeOr {_} _%I _%I _%I.
+Global Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
+Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
+Global Arguments KnownRMakeOr {_} _%I _%I _%I.
+Global Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
+
+Class MakeAffinely {PROP : bi} (P Q : PROP) :=
+  make_affinely : <affine> P ⊣⊢ Q.
+Global Arguments MakeAffinely {_} _%I _%I.
+Global Hint Mode MakeAffinely + - - : typeclass_instances.
+Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
+  known_make_affinely :> MakeAffinely P Q.
+Global Arguments KnownMakeAffinely {_} _%I _%I.
+Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
+
+Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
+  make_intuitionistically : □ P ⊣⊢ Q.
+Global Arguments MakeIntuitionistically {_} _%I _%I.
+Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
+Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
+  known_make_intuitionistically :> MakeIntuitionistically P Q.
+Global Arguments KnownMakeIntuitionistically {_} _%I _%I.
+Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
+
+Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
+  make_absorbingly : <absorb> P ⊣⊢ Q.
+Global Arguments MakeAbsorbingly {_} _%I _%I.
+Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
+Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
+  known_make_absorbingly :> MakeAbsorbingly P Q.
+Global Arguments KnownMakeAbsorbingly {_} _%I _%I.
+Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
+
+Class MakePersistently {PROP : bi} (P Q : PROP) :=
+  make_persistently : <pers> P ⊣⊢ Q.
+Global Arguments MakePersistently {_} _%I _%I.
+Global Hint Mode MakePersistently + - - : typeclass_instances.
+Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
+  known_make_persistently :> MakePersistently P Q.
+Global Arguments KnownMakePersistently {_} _%I _%I.
+Global Hint Mode KnownMakePersistently + ! - : typeclass_instances.
+
+Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
+  make_laterN : ▷^n P ⊣⊢ lP.
+Global Arguments MakeLaterN {_} _%nat _%I _%I.
+Global Hint Mode MakeLaterN + + - - : typeclass_instances.
+Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
+  known_make_laterN :> MakeLaterN n P lP.
+Global Arguments KnownMakeLaterN {_} _%nat _%I _%I.
+Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
+
+Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
+  make_except_0 : ◇ P ⊣⊢ Q.
+Global Arguments MakeExcept0 {_} _%I _%I.
+Global Hint Mode MakeExcept0 + - - : typeclass_instances.
+Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
+  known_make_except_0 :> MakeExcept0 P Q.
+Global Arguments KnownMakeExcept0 {_} _%I _%I.
+Global Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 860df49d9bca5e39f28eda07808aab78e8458172..c04c197827e0e59b3cf5a573df1f9eea9e259677 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -1,6 +1,6 @@
 From iris.bi Require Export monpred.
 From iris.bi Require Import plainly.
-From iris.proofmode Require Import proofmode modality_instances.
+From iris.proofmode Require Import proofmode classes_make modality_instances.
 From iris.prelude Require Import options.
 
 Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
diff --git a/iris/proofmode/proofmode.v b/iris/proofmode/proofmode.v
index 9397c0b96648b9e424a4c3025fe895bb11c90dd8..f22582b198b3721d4cfe424404c4f9c884ffc481 100644
--- a/iris/proofmode/proofmode.v
+++ b/iris/proofmode/proofmode.v
@@ -7,5 +7,6 @@ these files. *)
 From iris.proofmode Require Import class_instances class_instances_later
   class_instances_updates class_instances_embedding
   class_instances_plainly class_instances_internal_eq.
-From iris.proofmode Require Import class_instances_frame modality_instances.
+From iris.proofmode Require Import class_instances_frame class_instances_make.
+From iris.proofmode Require Import modality_instances.
 From iris.prelude Require Import options.