From 34062842e7890ec2ed4e73d4fdc27f61cb22e818 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 7 Apr 2020 15:13:37 +0200
Subject: [PATCH] Remark about space.

---
 docs/proof_mode.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index a8e11f8d1..1d8c8e37d 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -234,7 +234,8 @@ _introduction patterns_:
   will fail. We provide an implementation of the hook using Ltac2, which works
   with Coq 8.11, and can be installed with opam; see
   [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
-- `%` : move the hypothesis to the pure Coq context (anonymously).
+- `%` : move the hypothesis to the pure Coq context (anonymously). Note that if
+  `%` is followed by a string, and not another token, a space is needed.
 - `->` and `<-` : rewrite using a pure Coq equality
 - `# ipat` : move the hypothesis into the intuitionistic context. The tactic
   will fail if the hypothesis is not intuitionistic. On success, the tactic will
-- 
GitLab