diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 87fe3ef6568e3591523ef48d0b3c6c9146e27fe6..b9592351dbe077d9eb7ab2887ad1cde6e56ce92b 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1964,7 +1964,8 @@ Hint Extern 0 (_ ⊢ _) => iStartProof.
 
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (envs_entails _ _) => iPureIntro; try done.
-Hint Extern 0 (envs_entails _ _) => iAssumption.
+Hint Extern 0 (envs_entails _ ?Q) =>
+  first [is_evar Q; fail 1|iAssumption].
 Hint Extern 0 (envs_entails _ emp) => iEmpIntro.
 
 (* TODO: look for a more principled way of adding trivial hints like those
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index e8d30aa73c06313cb178265654ce9019abdbc1de..a79341f8a44eef7c657dcae213167430a5d1d6fc 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -86,6 +86,9 @@ Proof. eexists. iIntros "?" (P). iAssumption. Qed.
 Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P -∗ Q -∗ R -∗ Q.
 Proof. iIntros "H1 H2 H3". iAssumption. Qed.
 
+Lemma test_done_goal_evar Q : ∃ P, Q ⊢ P.
+Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.
+
 Lemma test_iDestruct_spatial_and P Q1 Q2 : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1.
 Proof. iIntros "[H [? _]]". by iFrame. Qed.
 
@@ -405,7 +408,7 @@ Lemma iFrame_with_evar_l P Q :
   ∃ R, (P -∗ Q -∗ R ∗ P) ∧ R = Q.
 Proof.
   eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
-  by iSplitR "HP". done.
+  iSplitR "HP"; iAssumption. done.
 Qed.
 Lemma iFrame_with_evar_persistent P Q :
   ∃ R, (P -∗ □ Q -∗ P ∗ R ∗ Q) ∧ R = emp%I.