diff --git a/CHANGELOG.md b/CHANGELOG.md
index 783b24183468e857b549eef50b1ef36d3ba7de8c..162142ed4d3228626fce4a28941389e4740f854a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,15 @@ way the logic is used on paper.  We also document changes in the Coq
 development; every API-breaking change should be listed, but not every new
 lemma.
 
+## Iris master
+
+**Changes in `proofmode`:**
+
+* `iAssumption` no longer instantiates evar premises with `False`. This used
+   to occur when the conclusion contains variables that are not in scope of the
+   evar, thus blocking the default behavior of instantiating the premise with
+   the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
+
 ## Iris 3.6.0 (2022-01-22)
 
 The highlights and most notable changes of this release are:
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 6f605be736a36b34f9dd5ccc2817a5af5b16a87f..8bed1396997bb86d079524b4dbc5fa630011fd0d 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -306,7 +306,8 @@ Tactic Notation "iAssumption" :=
           |exact Hass
           |pm_reduce; iSolveTC ||
            fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
-       |assert (P = False%I) as Hass by reflexivity;
+       |assert_fails (is_evar P); 
+        assert (P = False%I) as Hass by reflexivity;
         apply (tac_false_destruct _ j p P);
           [pm_reflexivity
           |exact Hass]
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index cd1337a5d1e5ee8c8507787fbaf8748380020901..cf81d3910ed4712dbb6a3e19df7e78f52cd00bf6 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -254,6 +254,10 @@ Tactic failure: iEval: %: unsupported selection pattern.
   â–· emp
 The command has indeed failed with message:
 Tactic failure: iFrame: cannot frame Q.
+The command has indeed failed with message:
+No applicable tactic.
+The command has indeed failed with message:
+No applicable tactic.
 "test_and_sep_affine_bi"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index aa055dc3b4aef3f7c2099de6fa9e8d5ff5668956..7d9fecc09c9fc5dca2e5e46b24682c7926b36e57 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -326,11 +326,6 @@ Definition tc_opaque_test : PROP := tc_opaque (∀ x : nat, ⌜ x = x ⌝)%I.
 Lemma test_iIntros_tc_opaque : ⊢ tc_opaque_test.
 Proof. by iIntros (x). Qed.
 
-(** Prior to 0b84351c this used to loop, now [iAssumption] instantiates [R] with
-[False] and performs false elimination. *)
-Lemma test_iAssumption_evar_ex_false : ∃ R, R ⊢ ∀ P, P.
-Proof. eexists. iIntros "?" (P). iAssumption. Qed.
-
 Lemma test_iApply_evar P Q R : (∀ Q, Q -∗ P) -∗ R -∗ P.
 Proof. iIntros "H1 H2". iApply "H1". iExact "H2". Qed.
 
@@ -978,12 +973,23 @@ Lemma test_iAssumption_evar P : ∃ R, (R ⊢ P) ∧ R = P.
 Proof.
   eexists. split.
   - iIntros "H". iAssumption.
-  (* Now verify that the evar was chosen as desired (i.e., it should not pick False). *)
-  - reflexivity.
+  - (* Verify that [iAssumption] instantiates the evar for the existential [R]
+    to become [P], and in particular, that it does not make it [False]. *)
+    reflexivity.
 Qed.
 
+(** Prior to 0b84351c this used to loop, now [iAssumption] fails. *)
 Lemma test_iAssumption_False_no_loop : ∃ R, R ⊢ ∀ P, P.
-Proof. eexists. iIntros "?" (P). done. Qed.
+Proof.
+  eexists. iIntros "H" (P).
+  (* Make sure that [iAssumption] does not perform False elimination on
+  hypotheses that are evars. *)
+  Fail iAssumption.
+  (* And neither does [done]. *)
+  Fail done.
+  (* But we can of course achieve that using an explicit proof. *)
+  iExFalso. iExact "H".
+Qed.
 
 Lemma test_apply_affine_impl `{!BiPlainly PROP} (P : PROP) :
   P -∗ (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q).