diff options
| author | Théo Zimmermann | 2019-04-29 14:19:30 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-04-29 14:19:30 +0200 |
| commit | 686894d47cfa548b4fa510c06c6bb08194dee5f7 (patch) | |
| tree | 77737cee52732bd296003db6119657c3efb989ba | |
| parent | eb227e5357d00ea039689b5af7a0e78cc345790d (diff) | |
| parent | 9116f7811db0eba707a6d49adcd3d96ca8669c46 (diff) | |
Merge PR #10018: Document unshelve (#3225)
Reviewed-by: Zimmi48
| -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 |