diff options
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 3 |
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:: |