From d04c9f7ed2676c2617421b0a01154adcbafc259e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 1 Mar 2019 12:58:42 +0100
Subject: [PATCH] Document [efoc] of [wp_pure].

---
 theories/heap_lang/proofmode.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 92851e213..fe7726148 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -65,6 +65,13 @@ Ltac wp_finish :=
   pm_prettify.        (* prettify â–·s caused by [MaybeIntoLaterNEnvs] and
                          λs caused by wp_value *)
 
+(** The argument [efoc] can be used to specify the construct that should be
+reduced. For example, you can write [wp_pure (EIf _ _ _)], which will search
+for an [EIf _ _ _] in the expression, and reduce it.
+
+The use of [open_constr] in this tactic is essential. It will convert all holes
+(i.e. [_]s) into evars, that later get unified when an occurences is found
+(see [unify e' efoc] in the code below). *)
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-- 
GitLab