1 files changed, 7 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 3c0577b8e4..4b1b7719c5 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -112,7 +112,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
       Aborts the editing of the proof named :token:`ident` (in case you have
       nested proofs).
 
-      .. seealso:: :opt:`Nested Proofs Allowed`
+      .. seealso:: :flag:`Nested Proofs Allowed`
 
    .. cmdv:: Abort All
 
@@ -200,13 +200,14 @@ The following options modify the behavior of ``Proof using``.
 
 
 .. opt:: Default Proof Using "@expression"
+   :name: Default Proof Using
 
    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
+.. flag:: Suggest Proof Using
 
    When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not
    provide one.
@@ -453,6 +454,7 @@ The following example script illustrates all these features:
 Set Bullet Behavior
 ```````````````````
 .. opt:: Bullet Behavior  %( "None" %| "Strict Subproofs" %)
+   :name: Bullet Behavior
 
    This option controls the bullet behavior and can take two possible values:
 
@@ -585,6 +587,7 @@ Controlling the effect of proof editing commands
 
 
 .. opt:: Hyps Limit @num
+   :name: Hyps Limit
 
    This option controls the maximum number of hypotheses displayed in goals
    after the application of a tactic. All the hypotheses remain usable
@@ -593,7 +596,7 @@ Controlling the effect of proof editing commands
    available hypotheses.
 
 
-.. opt:: Automatic Introduction
+.. flag:: Automatic Introduction
 
    This option controls the way binders are handled
    in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the
@@ -605,7 +608,7 @@ Controlling the effect of proof editing commands
    has to be used to move the assumptions to the local context.
 
 
-.. opt:: Nested Proofs Allowed
+.. flag:: Nested Proofs Allowed
 
    When turned on (it is off by default), this option enables support for nested
    proofs: a new assertion command can be inserted before the current proof is