From 7e9c378e11b2ed480dd459e75c80ed408589d5ae Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Jul 2016 21:12:12 +0200
Subject: [PATCH] More proof mode docs.

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

diff --git a/ProofMode.md b/ProofMode.md
index 692c7568c..8ffaa46bc 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -56,6 +56,8 @@ Elimination of logical connectives
   quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
   object level connectives using the proof mode introduction patterns
   `ipat1 ... ipatn`.
+- `iDestruct trm as %cpat : elimination of a pure hypothesis using the Coq
+   introduction pattern `cpat`.
 
 Separating logic specific tactics
 ---------------------------------
-- 
GitLab