diff --git a/CHANGELOG.md b/CHANGELOG.md
index d3277110e58796027eb3682babedcde453678de4..d10badce458550810d01b51979a7dbf457b491da 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -78,6 +78,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
    `not_stuck_fill` → `not_stuck_fill_inv`.
   - Use the non-`_inv` names (that freed up) for the forwards directions:
    `reducible_fill`, `reducible_no_obs_fill`, `irreducible_fill_inv`.
+* The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context.
 
 **Changes in heap_lang:**
 
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index f87591b57ab330f777954027a7878176a04149d2..89e55555f5295592d0a2c2ede462748f07ad7d96 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -24,7 +24,10 @@ Applying hypotheses and lemmas
 ------------------------------
 
 - `iExact "H"`  : finish the goal if the conclusion matches the hypothesis `H`
-- `iAssumption` : finish the goal if the conclusion matches any hypothesis
+- `iAssumption` : finish the goal if the conclusion matches any hypothesis in
+  either the proofmode or the Coq context. Only hypotheses in the Coq context
+  that are _syntactically_ of the shape `⊢ P` are recognized by this tactic
+  (this means that assumptions of the shape `P ⊢ Q` are not recognized).
 - `iApply pm_trm` : match the conclusion of the current goal against the
   conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
   proof mode terms below.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index e45044a8275bdffdd30a5d1326d2afff652df913..6643f7b8118fbd7923adb0231fcf18c1603d1164 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -515,8 +515,7 @@ Tactic failure: iExact: "HQ" not found.
 The command has indeed failed with message:
 Tactic failure: iExact: "HQ" : Q does not match goal.
 The command has indeed failed with message:
-Tactic failure: iExact: "HP"
-not absorbing and the remaining hypotheses not affine.
+Tactic failure: iExact: remaining hypotheses not affine and the goal not absorbing.
 "iClear_fail"
      : string
 The command has indeed failed with message:
@@ -581,13 +580,19 @@ Tactic failure: iApply: cannot apply P.
 "iApply_fail_not_affine_1"
      : string
 The command has indeed failed with message:
-Tactic failure: iApply: Q
-not absorbing and the remaining hypotheses not affine.
+Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing.
 "iApply_fail_not_affine_2"
      : string
 The command has indeed failed with message:
-Tactic failure: iApply: Q
-not absorbing and the remaining hypotheses not affine.
+Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing.
+"iAssumption_fail_not_affine_1"
+     : string
+The command has indeed failed with message:
+Tactic failure: iAssumption: remaining hypotheses not affine and the goal not absorbing.
+"iAssumption_fail_not_affine_2"
+     : string
+The command has indeed failed with message:
+Tactic failure: iAssumption: remaining hypotheses not affine and the goal not absorbing.
 "iRevert_wrong_var"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e1c4ad8130edbb6d8f0ca792cb4b73ff0cf7d483..1c51da0645d7f0229fd5cd15ee1199b982a4b0b3 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -316,6 +316,12 @@ Proof. iIntros "H". iMod "H". done. Qed.
 Lemma test_iAssumption_False P : False -∗ P.
 Proof. iIntros "H". done. Qed.
 
+Lemma test_iAssumption_coq_1 P Q : (⊢ Q) → <affine> P -∗ Q.
+Proof. iIntros (HQ) "_". iAssumption. Qed.
+
+Lemma test_iAssumption_coq_2 P Q : (⊢ □ Q) → <affine> P -∗ ▷ Q.
+Proof. iIntros (HQ) "_". iAssumption. Qed.
+
 (* Check instantiation and dependent types *)
 Lemma test_iSpecialize_dependent_type (P : ∀ n, vec nat n → PROP) :
   (∀ n v, P n v) -∗ ∃ n v, P n v.
@@ -1018,9 +1024,17 @@ Lemma iApply_fail_not_affine_1 P Q : P -∗ Q -∗ Q.
 Proof. iIntros "HP HQ". Fail iApply "HQ". Abort.
 
 Check "iApply_fail_not_affine_2".
-Lemma iApply_fail_not_affine_1 P Q R : P -∗ R -∗ (R -∗ Q) -∗ Q.
+Lemma iApply_fail_not_affine_2 P Q R : P -∗ R -∗ (R -∗ Q) -∗ Q.
 Proof. iIntros "HP HR HQ". Fail iApply ("HQ" with "HR"). Abort.
 
+Check "iAssumption_fail_not_affine_1".
+Lemma iAssumption_fail_not_affine_1 P Q : P -∗ Q -∗ Q.
+Proof. iIntros "HP HQ". Fail iAssumption. Abort.
+
+Check "iAssumption_fail_not_affine_2".
+Lemma iAssumption_fail_not_affine_2 P Q : (⊢ Q) → P -∗ Q.
+Proof. iIntros (HQ) "HP". Fail iAssumption. Abort.
+
 Check "iRevert_wrong_var".
 Lemma iRevert_wrong_var (k : nat) (Φ : nat → PROP) : ⊢ Φ (S k).
 Proof.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 8d38f7f972ed3fbd6f1e3f00a4f89d653ff62792..d9613c1fedea5eb3417fd7028244f9799408cdc9 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -91,6 +91,21 @@ Proof.
   - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
 Qed.
 
+Lemma tac_assumption_coq Δ P Q :
+  (⊢ P) →
+  FromAssumption true P Q →
+  (if env_spatial_is_nil Δ then TCTrue
+   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ))) →
+  envs_entails Δ Q.
+Proof.
+  rewrite /FromAssumption /bi_emp_valid /= => HP HPQ H.
+  rewrite envs_entails_eq -(left_id emp%I bi_sep (of_envs Δ)).
+  rewrite -bi.intuitionistically_emp HP HPQ.
+  destruct (env_spatial_is_nil _) eqn:?.
+  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
+  - destruct H; by rewrite sep_elim_l.
+Qed.
+
 Lemma tac_rename Δ i j p P Q :
   envs_lookup i Δ = Some (p,P) →
   match envs_simple_replace i p (Esnoc Enil j P) Δ with
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 418f25c0db18669065a873a724773286758e2099..30bbab30d5801e4a5fc6364c93d8f806520f1e01 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -243,7 +243,7 @@ Tactic Notation "iExact" constr(H) :=
      fail "iExact:" H ":" P "does not match goal"
     |pm_reduce; iSolveTC ||
      let H := pretty_ident H in
-     fail "iExact:" H "not absorbing and the remaining hypotheses not affine"].
+     fail "iExact: remaining hypotheses not affine and the goal not absorbing"].
 
 Tactic Notation "iAssumptionCore" :=
   let rec find Γ i P :=
@@ -261,6 +261,17 @@ Tactic Notation "iAssumptionCore" :=
      is_evar i; first [find Γp i P | find Γs i P]; pm_reflexivity
   end.
 
+Tactic Notation "iAssumptionCoq" :=
+  let Hass := fresh in
+  match goal with
+  | H : ⊢ ?P |- envs_entails _ ?Q =>
+     pose proof (_ : FromAssumption true P Q) as Hass;
+     notypeclasses refine (tac_assumption_coq _ P _ H _ _);
+       [exact Hass
+       |pm_reduce; iSolveTC ||
+        fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
+  end.
+
 Tactic Notation "iAssumption" :=
   let Hass := fresh in
   let rec find p Γ Q :=
@@ -269,9 +280,9 @@ Tactic Notation "iAssumption" :=
        [pose proof (_ : FromAssumption p P Q) as Hass;
         eapply (tac_assumption _ j p P);
           [pm_reflexivity
-          |apply Hass
+          |exact Hass
           |pm_reduce; iSolveTC ||
-           fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"]
+           fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
        |assert (P = False%I) as Hass by reflexivity;
         apply (tac_false_destruct _ j p P);
           [pm_reflexivity
@@ -280,7 +291,9 @@ Tactic Notation "iAssumption" :=
     end in
   lazymatch goal with
   | |- envs_entails (Envs ?Γp ?Γs _) ?Q =>
-     first [find true Γp Q | find false Γs Q
+     first [find true Γp Q
+           |find false Γs Q
+           |iAssumptionCoq
            |fail "iAssumption:" Q "not found"]
   end.
 
@@ -1142,7 +1155,7 @@ Local Ltac iApplyHypExact H :=
        |pm_reduce; iSolveTC]
     |lazymatch iTypeOf H with
      | Some (_,?Q) =>
-        fail 2 "iApply:" Q "not absorbing and the remaining hypotheses not affine"
+        fail 2 "iApply: remaining hypotheses not affine and the goal not absorbing"
      end].
 Local Ltac iApplyHypLoop H :=
   first