diff --git a/CHANGELOG.md b/CHANGELOG.md
index efce126461ce7c8ea5bd71174841f79b265e0503..ac2d07301e3b3550dfbd6c8ee26b7a599acf216a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -41,6 +41,10 @@ lemma.
   Proofs that are generic in `PROP` might have to add those new classes as
   assumptions to remain compatible, and code that instantiates the BI interface
   needs to provide instances for the new classes.
+* Make `frame_fractional` not an instance any more; instead fractional
+  propositions that want to support framing are expected to register an
+  appropriate instance themselves. HeapLang and gen_heap `↦` still support
+  framing, but the other fractional propositions in Iris do not.
 
 **Changes in `heap_lang`:**
 
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 467b9f90cd1c695b3d2ab0e5c16ef6f9e404d63e..7df5ef405a90123ef77dca3a226b8f9d53417092 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -177,6 +177,12 @@ Section gen_heap.
   Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
   Proof. rewrite mapsto_eq. apply ghost_map_elem_persist. Qed.
 
+  (** Framing support *)
+  Global Instance frame_mapsto p l v q1 q2 RES :
+    FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
+    Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.
+  Proof. apply: frame_fractional. Qed.
+
   (** General properties of [meta] and [meta_token] *)
   Global Instance meta_token_timeless l N : Timeless (meta_token l N).
   Proof. rewrite meta_token_eq. apply _. Qed.
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 8a061d6894f7e2c0205cfa633ef1f55ea2c96145..9b48116c8ac43250d1f60c7b2889a1b782dca1bb 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -194,10 +194,13 @@ Section fractional.
   Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
     frame_fractional_hyps_half.
 
-  Global Instance frame_fractional p R r Φ P q RES:
+  (* Not an instance because of performance; you can locally add it if you are
+  willing to pay the cost. We have concrete instances for certain fractional
+  assertions such as ↦. *)
+  Lemma 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. (* No explicit priority, as default prio > [frame_here]'s 1. *)
+    Frame p R P RES.
   Proof.
     rewrite /Frame=>-[HR _][->?]H.
     revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 1c4d73212719176c83e45444075d63fb1581a3b3..0e80ada63a78541a97c6b73c5e050b5486fd5cc2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -373,6 +373,14 @@ Section mapsto_tests.
     l ↦{#1 / 2} v -∗  ∃ q, l ↦{#1 / 2 + q} v.
   Proof. iIntros "H". iExists _. iSplitL; first by iAssumption. Abort.
 
+  Lemma mapsto_frame_1 l v q1 q2 :
+    l ↦{#q1} v -∗ l ↦{#q2} v -∗ l ↦{#q1 + q2} v.
+  Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.
+
+  Lemma mapsto_frame_2 l v q :
+    l ↦{#q/2} v -∗ l ↦{#q/2} v -∗ l ↦{#q} v.
+  Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.
+
 End mapsto_tests.
 
 Section inv_mapsto_tests.