debug trivial and debug auto were not in the tactic index.

1 files changed, 3 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 76796c934f..5673b496e6 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3134,6 +3134,7 @@ hints of the database named core.
    to know what lemmas/assumptions were used.
 
 .. tacv:: debug auto
+   :name: debug auto
 
    Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal,
    including failing paths.
@@ -3153,7 +3154,9 @@ hints of the database named core.
 .. tacv:: trivial with *
 .. tacv:: trivial using {+ @lemma}
 .. tacv:: debug trivial
+   :name: debug trivial
 .. tacv:: info_trivial
+   :name: info_trivial
 .. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}}
 
 .. note::