From 7e706e0fe8a8fac88abc90bf476bcaf0f4b3fa76 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 17 Aug 2018 18:36:19 +0200
Subject: Define bullet production token.

---
 doc/sphinx/proof-engine/proof-handling.rst | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index d1a70b5619..e9aacba3a5 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -358,8 +358,10 @@ same bullet ``b``. See the example below.
 
 Different bullets can be used to nest levels. The scope of bullet does
 not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further
-nesting levels provided they are delimited by these. Available bullets
-are ``-``, ``+``, ``*``, ``--``, ``++``, ``**``, ``---``, ``+++``, ``***``, ... (without a terminating period).
+nesting levels provided they are delimited by these. Bullets are made of
+repeated ``-``, ``+`` or ``*`` symbols:
+
+.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * }
 
 Note again that when a focused goal is proved a message is displayed
 together with a suggestion about the right bullet or ``}`` to unfocus it
-- 
cgit v1.2.3