From 1c105c7de2a29d54623f46034900c58df7ac60f3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Wed, 13 Jul 2022 15:55:15 +0000
Subject: [PATCH] clarify

---
 docs/heap_lang.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/docs/heap_lang.md b/docs/heap_lang.md
index 705480cd1..7cbfd5e4e 100644
--- a/docs/heap_lang.md
+++ b/docs/heap_lang.md
@@ -105,7 +105,10 @@ Further tactics:
   applying `wp_bind` as needed.  See the [ProofMode docs](./proof_mode.md) for an
   explanation of `pm_trm`.
 - `wp_smart_apply pm_trm`: like `wp_apply`, but also performs pure reduction
-  steps (same as `wp_pure`) to reveal a redex that matches `pm_trm`.
+  steps to reveal a redex that matches `pm_trm`. Precisely, if applying the
+  lemma fails, `wp_smart_apply` will perform a step of pure reduction (via
+  `wp_pure`), and repeat. (This means that `wp_smart_apply` is not the same
+  as `wp_pures; wp_apply`.)
 
 There is no tactic for `Fork`, just do `wp_apply wp_fork`.
 
-- 
GitLab