diff options
| author | Clément Pit-Claudel | 2018-10-13 23:01:13 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-10-13 23:01:13 -0400 |
| commit | 19618d289465f4c609b70810286c40fe9e35b21a (patch) | |
| tree | e7fcf659a3304e2307928788eeccc75926b6ccd1 | |
| parent | 235cb6e6c243863b7270d273ceeef681eb350247 (diff) | |
| parent | d0927f469975a75bbcd8cba7202097f56a5ff9ba (diff) | |
Merge PR #8652: Add missing indexes for Hint Cut and Hint Mode.
| -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 |