aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClément Pit-Claudel2018-08-29 17:04:40 -0400
committerClément Pit-Claudel2018-08-29 17:04:40 -0400
commit3825a76c94eca41a3aa16c7cd624bc3ce776c365 (patch)
tree9b4106fbefece1fcce1aeb8dc46542b228c1f916
parent06a00cf53442dacafd578b8db655e5d8097e9d84 (diff)
parent1b0e2daa3050e135ae44c23b6924e305bd59a873 (diff)
Merge PR #8345: Add index for focusing braces.
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst5
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index b49d0f0504..fe2124502a 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -315,6 +315,9 @@ Navigation in the proof tree
.. _curly-braces:
+.. index:: {
+ }
+
.. cmd:: %{ %| %}
The command ``{`` (without a terminating period) focuses on the first
@@ -369,7 +372,7 @@ Navigation in the proof tree
Brackets are used to focus on a single goal given either by its position
or by its name if it has one.
- .. seealso:: The error messages about bullets below.
+ .. seealso:: The error messages about bullets below.
.. _bullets: