diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 92851e21392ece4904ec055e61f96694d512e84e..fe772614870bd10ba047cc70ff152c0d24e4094c 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