From 8b49eacf694b23e09d2c4108250893df5506febd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Jan 2018 17:21:54 +0100
Subject: [PATCH] Documentation.

---
 ProofMode.md | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index cc19fdf3d..06ba8e1c8 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -150,11 +150,22 @@ Induction
   variables `x1 ... xn`, the hypotheses given by the selection pattern `selpat`,
   and the spatial context.
 
-Rewriting
----------
+Rewriting / simplification
+--------------------------
+
+- `iRewrite pm_trm` / `iRewrite pm_trm in "H"` : rewrite using an internal
+  equality in the proof mode goal / hypothesis `H`.
+- `iEval (tac)` / `iEval (tac) in H` : performs a tactic `tac` on the proof mode
+  goal / hypothesis `H`. The tactic `tac` should be a reduction or rewriting
+  tactic like `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
+  tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar` where `P`
+  is the proof goal / hypothesis `H`. After running `tac`, `?evar` is unified
+  with the resulting `P`, which in turn becomes the new proof mode goal /
+  hypothesis `H`.
+  Note that parentheses around `tac` are needed.
+- `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal /
+  hypothesis `H`. This is a shorthand for `iEval (simpl)`.
 
-- `iRewrite pm_trm` : rewrite an equality in the conclusion.
-- `iRewrite pm_trm in "H"` : rewrite an equality in the hypothesis `H`.
 
 Iris
 ----
-- 
GitLab