Add docs and CHANGELOG.

CHANGELOG.md

@@ -19,6 +19,7 @@ lemma.
   invariant opening.
 * Change `iInduction` to always generate a magic wand instead of sometimes
   generating an implication for reverted hypotheses.
+* Add `iUnfold` tactic.
 
 **Changes in `base_logic`:**
 

docs/proof_mode.md

@@ -273,6 +273,10 @@ Rewriting / simplification
 - `iSimpl` / `iSimpl in "selpat"` : perform `simpl` on the proof mode
   goal / hypotheses given by the selection pattern `selpat`. This is a
   shorthand for `iEval (simpl)`.
+- `iUnfold xs` / `iUnfold xs in "selpat"` : perform `unfold xs` on the proof
+  mode goal / hypotheses given by the selection pattern `selpat`. This is a
+  shorthand for `iEval (unfold xs)`. Similar to Coq's `unfold`, the argument
+  `xs` should be a comma-separated non-empty list.
 
 Iris
 ----