From 9116f7811db0eba707a6d49adcd3d96ca8669c46 Mon Sep 17 00:00:00 2001
From: Paolo G. Giarrusso
Date: Sat, 27 Apr 2019 16:56:50 +0200
Subject: 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).
---
 doc/sphinx/proof-engine/tactics.rst | 6 ++++++
 1 file changed, 6 insertions(+)

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
 
-- 
cgit v1.2.3