Clean-up around options.

- Remove all trailing dots.
- There is only one Bullet Behavior option.
- Replaces `@natural` and `@integer` by `@num`.

1 files changed, 7 insertions, 12 deletions

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 64e28cea43..53205b6193 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -95,7 +95,7 @@ has been opened using the ``Goal`` command.
 .. cmd:: Admitted.
    :name: Admitted (interactive proof)
 
-This command is available in interactive editing proof mode to give up
+This command is available in interactive editing mode to give up
 the current proof and declare the initial goal as an axiom.
 
 .. cmd:: Proof @term.
@@ -185,14 +185,14 @@ Proof using options
 The following options modify the behavior of ``Proof using``.
 
 
-.. opt:: Default Proof Using "@expression".
+.. opt:: Default Proof Using "@expression"
 
    Use :n:`@expression` as the default ``Proof``` using value. E.g. ``Set Default
    Proof Using "a b"``. will complete all ``Proof`` commands not followed by a
    using part with using ``a`` ``b``.
 
 
-.. opt:: Suggest Proof Using.
+.. opt:: Suggest Proof Using
 
    When ``Qed`` is performed, suggest a using annotation if the user did not
    provide one.
@@ -427,17 +427,12 @@ You just finished a goal focused by ``{``, you must unfocus it with ``}``.
 
 Set Bullet Behavior
 ```````````````````
+.. opt:: Bullet Behavior  %( "None" %| "Strict Subproofs" %)
 
-The bullet behavior can be controlled by the following commands.
-
-.. opt:: Bullet Behavior "None"
-
-This makes bullets inactive.
-
-.. opt:: Bullet Behavior "Strict Subproofs"
-
-This makes bullets active (this is the default behavior).
+   This option controls the bullet behavior and can take two possible values:
 
+   - "None": this makes bullets inactive.
+   - "Strict Subproofs": this makes bullets active (this is the default behavior).
 
 .. _requestinginformation: