diff options
| author | Paolo G. Giarrusso | 2019-04-27 16:56:50 +0200 |
|---|---|---|
| committer | Paolo G. Giarrusso | 2019-04-29 03:27:48 +0200 |
| commit | 9116f7811db0eba707a6d49adcd3d96ca8669c46 (patch) | |
| tree | 809f8acb90991dc65410d77aaad62601d8289498 | |
| parent | ae4239d6a5f4afcd9b7321dba790ffd4a64994a1 (diff) | |
Document unshelve (#3225)
I believe this is the appropriate place for users to read about this, even tho
`unshelve` is technically a tactical.
This example was explicitly requested in #3225 and is commonly used in both
Iris (and was documented in the changelog at the time).
| -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 |