From 62d5e8b58f72c14caf1b147252e18f0992a42494 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 26 Feb 2020 09:07:29 +0100
Subject: [PATCH] Add documentation. Thanks to @Blaisorblade.

---
 docs/style_guide.md | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/docs/style_guide.md b/docs/style_guide.md
index 65fd05759..6254f167b 100644
--- a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ -32,6 +32,21 @@ Typeclasses Opaque join_handle.
 This makes sure that the proof mode does not "look into" your definition when it
 is used by clients.
 
+## Notations
+
+Notations starting with `(` or `{` should be left at their default level (`0`),
+and inner subexpressions that are bracketed by delimiters should be left at
+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.
+
+For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules).
+
 ## Naming conventions for variables/arguments/hypotheses
 
 ### small letters
-- 
GitLab