From c98ea2a5b0e83b446697d784e5940690b5443417 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Aug 2016 15:26:09 +0200
Subject: [PATCH] Document iFrame without arguments.

---
 ProofMode.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/ProofMode.md b/ProofMode.md
index ed7f78881..cefa97d97 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -70,7 +70,9 @@ Elimination of logical connectives
 Separating logic specific tactics
 ---------------------------------
 
-- `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal. 
+- `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal. When
+  `iFrame` is called without arguments, it attempts to frame all spatial
+  hypotheses.
 - `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
   `H : P1 ★ P2`.
 
-- 
GitLab