From 19f88e47ca4ca6de8b5bf2d5c9bb46a3cbdaf411 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 27 Oct 2017 14:39:47 +0200
Subject: [PATCH] Tweak the proof mode docs.

---
 ProofMode.md | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index f7018ae66..cc19fdf3d 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -121,10 +121,12 @@ Modalities
   an instance of the `ElimModal` type class. Instances include: later, except 0,
   basic update and fancy update.
 
-The persistence modality
-------------------------
+The persistence and plainness modalities
+----------------------------------------
 
-- `iAlways` is a synonym for `iIntros "!#"`.
+- `iAlways` : introduce a persistence or plainness modality and the spatial
+  context. In case of a plainness modality, the tactic will prune all persistent
+  hypotheses that are not plain.
 
 The later modality
 ------------------
@@ -213,10 +215,8 @@ appear at the top level:
   Items of the selection pattern can be prefixed with `$`, which cause them to
   be framed instead of cleared.
 - `!%` : introduce a pure goal (and leave the proof mode).
-- `!#` : introduce an persistence or plainness modality and clear the spatial
-  context. In case of a plainness modality, it will prune all persistent
-  hypotheses that are not plain.
-- `!>` : introduce a modality.
+- `!#` : introduce an persistence or plainness modality (by calling `iAlways`).
+- `!>` : introduce a modality (by calling `iModIntro`).
 - `/=` : perform `simpl`.
 - `//` : perform `try done` on all goals.
 - `//=` : syntactic sugar for `/= //`
-- 
GitLab