Add missing indexes for Hint Cut and Hint Mode.

1 files changed, 2 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index db9f04ba11..794804a1f6 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3513,6 +3513,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
             Info 1 auto with eqdec.
 
    .. cmdv:: Hint Cut @regexp
+      :name: Hint Cut
 
       .. warning::
 
@@ -3546,6 +3547,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       initial cut expression being `emp`.
 
    .. cmdv:: Hint Mode @qualid {* (+ | ! | -)}
+      :name: Hint Mode
 
       This sets an optional mode of use of the identifier :n:`@qualid`. When
       proof-search faces a goal that ends in an application of :n:`@qualid` to