From d7d41bee6ae195a7842c40d84162eb1e26a24533 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Sep 2020 18:40:11 +0200
Subject: Fixing documentation relatively to example of use of extra spaces in
 notations.

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 9e8e5e5fa5..8857f6b484 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -241,12 +241,12 @@ notation is the insertion of spaces at some places of the notation.
 This is performed by adding extra spaces between the symbols and
 parameters: each extra space (other than the single space needed to
 separate the components) is interpreted as a space to be inserted by
-the printer. Here is an example showing how to add spaces around the
-bar of the notation.
+the printer. Here is an example showing how to add spaces next to the
+curly braces.
 
 .. coqtop:: in
 
-   Notation "{{ x : A | P }}" := (sig (fun x : A => P)) (at level 0, x at level 99).
+   Notation "{{  x : A | P  }}" := (sig (fun x : A => P)) (at level 0, x at level 99).
 
 .. coqtop:: all
 
-- 
cgit v1.2.3