From d0927f469975a75bbcd8cba7202097f56a5ff9ba Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 4 Oct 2018 12:49:25 +0200
Subject: Add missing indexes for Hint Cut and Hint Mode.

---
 doc/sphinx/proof-engine/tactics.rst | 2 ++
 1 file changed, 2 insertions(+)

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
-- 
cgit v1.2.3