From 60d28bbbb0eed2fc35fdbea6382fff5de9ced4be Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Apr 2019 08:56:57 +0200
Subject: [PATCH] Document `iAccu`.

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

diff --git a/ProofMode.md b/ProofMode.md
index b165c01a5..9d2220a73 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -111,6 +111,9 @@ Separation logic-specific tactics
   framed.
 - `iCombine "H1" "H2" as "pat"` : combines `H1 : P1` and `H2 : P2` into
   `H: P1 ∗ P2`, then calls `iDestruct H as pat` on the combined hypothesis.
+- `iAccu` : solves a goal that is an evar by instantiating it with a all
+  hypotheses from the spatial context joined together with a separating
+  conjunction (or `emp` in case the spatial context is empty).
 
 Modalities
 ----------
-- 
GitLab