diff options
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index e6922408aa..8d9e99b9d5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4724,6 +4724,12 @@ Non-logical tactics from the shelf into focus, by appending them to the end of the current list of focused goals. +.. tacn:: unshelve @tactic + :name: unshelve + + Performs :n:`@tactic`, then unshelves existential variables added to the + shelf by the execution of :n:`@tactic`, prepending them to the current goal. + .. tacn:: give_up :name: give_up |