From 83184356199cde91eae3ccf642e215f9c1e804c0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 4 Aug 2017 16:54:09 +0200
Subject: [PATCH] Document elimination of spatial conjunctions.

---
 ProofMode.md | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index d178f52f0..2eaab453a 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -188,8 +188,13 @@ _introduction patterns_:
 - `?` : create an anonymous hypothesis.
 - `_` : remove the hypothesis.
 - `$` : frame the hypothesis in the goal.
-- `[ipat ipat]` : (separating) conjunction elimination.
-- `[ipat|ipat]` : disjunction elimination.
+- `[ipat1 ipat2]` : (separating) conjunction elimination. In order to eliminate
+  conjunctions `P âˆ§ Q` in the spatial context, one of the following conditions
+  should hold:
+  + Either the proposition `P` or `Q` should be persistent.
+  + Either `ipat1` or `ipat2` should be `_`, which results in one of the
+    conjuncts to be thrown away.
+- `[ipat1|ipat2]` : disjunction elimination.
 - `[]` : false elimination.
 - `%` : move the hypothesis to the pure Coq context (anonymously).
 - `# ipat` : move the hypothesis to the persistent context.
-- 
GitLab