From 0502e7d201fd91e535bfc129e96efc9537523e50 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jan 2019 10:40:47 +0100
Subject: [PATCH] Document `iRewrite -...` in the proof mode docs.

This commit closes issue #192.
---
 ProofMode.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/ProofMode.md b/ProofMode.md
index 389afb3cf..37020c3d8 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -146,6 +146,8 @@ Rewriting / simplification
 
 - `iRewrite pm_trm` / `iRewrite pm_trm in "H"` : rewrite using an internal
   equality in the proof mode goal / hypothesis `H`.
+- `iRewrite -pm_trm` / `iRewrite -pm_trm in "H"` : rewrite in reverse direction
+  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`
-- 
GitLab