From af197fa42e5e2938975a79b6974247ed04262d68 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 26 Feb 2020 13:39:17 +0100
Subject: [PATCH] slightly expand notation docs

---
 docs/proof_guide.md | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index b07e06df8..8de113129 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -295,10 +295,13 @@ their default level (`200`).
 
 Moreover, correct parsing of notations sometimes relies on Coq's automatic
 left-factoring, which can require coordinating levels of certain "conflicting"
-notations and their subexpressions. For instance, to disambiguate `(⊢@{ PROP })`
-and `(⊢@{ PROP } P)`, Coq must factor out a nonterminal for `⊢@{ PROP }`, but it
-can only do so if all occurrences of `⊢@{ PROP }` agree on the precedences for
-all subexpressions.
+notations and their subexpressions.  For instance, to disambiguate `(⊢@{ PROP
+})` and `(⊢@{ PROP } P)`, Coq must factor out a nonterminal for `⊢@{ PROP }`,
+but it can only do so if all occurrences of `⊢@{ PROP }` agree on the
+precedences for all subexpressions. This also requires using the same
+tokenization in all cases, i.e., the notation has to consistently be declared as
+`(⊢@{` or `('⊢@{'`, but not a mixture of the two. The latter form of using
+explicit tokenization with `'` is preferred to avoid relying on Coq's default.
 
 For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules).
 
-- 
GitLab