From ba3f6ce2dffc92f6ad724afa8ab42f02714c6d07 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 20 Mar 2020 11:26:27 +0100
Subject: [PATCH] Add documentation.

---
 docs/proof_mode.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index f87591b57..89e55555f 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.
-- 
GitLab