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.