More general instance for framing under `<affine>`.

tests/proofmode.v

@@ -455,6 +455,13 @@ Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
 Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
 Proof. iIntros "H1 H2". by iFrame "H1". Qed.
 
+Lemma test_iFrame_affinely_1 P Q `{!Affine P} :
+  P -∗ <affine> Q -∗ <affine> (P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} :
+  P -∗ Q -∗ <affine> (P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+
 Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
 Proof.
   iIntros "HF".

theories/proofmode/frame_instances.v

@@ -204,11 +204,12 @@ Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_em
 Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
 Proof. by rewrite /MakeAffinely. Qed.
 
-Global Instance frame_affinely R P Q Q' :
-  Frame true R P Q → MakeAffinely Q Q' → Frame true R (<affine> P) Q'.
+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'.
 Proof.
-  rewrite /Frame /MakeAffinely=> <- <- /=.
-  rewrite -{1}(affine_affinely (□ R)%I) affinely_sep_2 //.
+  rewrite /Frame /MakeAffinely=> -[->|?] <- <- /=;
+    by rewrite -{1}(affine_affinely (_ R)%I) affinely_sep_2.
 Qed.
 
 Global Instance make_intuitionistically_emp :