From 77695c5f54807090bc87e8ad77d1728c4e7a0436 Mon Sep 17 00:00:00 2001
From: Mackie Loeffel <mackie.loeffel@web.de>
Date: Wed, 23 Jan 2019 10:20:54 +0100
Subject: [PATCH] Added note about unicode asterisk to docs

---
 ProofMode.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 3c7e21642..a6446801c 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -101,7 +101,8 @@ Separation logic-specific tactics
 
   + `%` : repeatedly frame hypotheses from the Coq context.
   + `#` : repeatedly frame hypotheses from the intuitionistic context.
-  + `∗` : frame as much of the spatial context as possible.
+  + `∗` : frame as much of the spatial context as possible. (N.B: this
+          is the unicode symbol `∗`, not the regular asterisk `*`.)
 
   Notice that framing spatial hypotheses makes them disappear, but framing Coq
   or intuitionistic hypotheses does not make them disappear.
@@ -189,7 +190,8 @@ following _selection patterns_:
 - `H` : select the hypothesis named `H`.
 - `%` : select the entire pure/Coq context.
 - `#` : select the entire intuitionistic context.
-- `∗` : select the entire spatial context.
+- `∗` : select the entire spatial context. (N.B: this
+        is the unicode symbol `∗`, not the regular asterisk `*`.)
 
 Introduction patterns
 =====================
-- 
GitLab