Merge branch 'ralf/smart-apply' into 'master'

document wp_smart_apply

See merge request iris/iris!811

docs/heap_lang.md

@@ -104,6 +104,11 @@ Further tactics:
 - `wp_apply pm_trm`: Apply a lemma whose conclusion is a `WP`, automatically
   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 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`.