aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2018-08-28 16:34:28 +0200
committerThéo Zimmermann2018-08-28 16:34:28 +0200
commit1b0e2daa3050e135ae44c23b6924e305bd59a873 (patch)
tree065d7e34e3eb5f2bb17cd8a817ce03ee6605adc9
parenta57891211e578605f6cb7e05f5fdadd7de49e519 (diff)
Add index for focusing braces.
And fix wrong indentation.
-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: