From 9fdf7d254bdf821ca69228420ed8123455ead099 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 Jan 2017 12:41:02 +0100
Subject: [PATCH] Improve documentation of iApply.

---
 ProofMode.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/ProofMode.md b/ProofMode.md
index 8583f742e..a97d988d0 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -16,6 +16,12 @@ Applying hypotheses and lemmas
 - `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.
+  If the applied term has more premises than the number of given specialization
+  patterns, all remaining spatial hypotheses go to the first premise that does
+  not have corresponding specialization pattern. Subsequent premises without
+  specialization pattern do not get any spatial hypotheses. In other words, the
+  specialization pattern is extended with `[-] [] ... []` to account for
+  hypotheses without specialization pattern.
 
 Context management
 ------------------
-- 
GitLab