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