From 16706383de6035d3f75b539a73898eb1c0fc0778 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 Nov 2020 12:01:20 +0100
Subject: Document the deprecation of the commands.

---
 doc/sphinx/proofs/writing-proofs/proof-mode.rst | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
index fd8a0329d6..40d032543f 100644
--- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst
+++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
@@ -288,12 +288,18 @@ Name a set of section hypotheses for ``Proof using``
    existential variables remain. To instantiate existential variables
    during proof edition, you should use the tactic :tacn:`instantiate`.
 
+   .. deprecated:: 8.13
+
 .. cmd:: Grab Existential Variables
 
    This command can be run when a proof has no more goal to be solved but
    has remaining uninstantiated existential variables. It takes every
    uninstantiated existential variable and turns it into a goal.
 
+   .. deprecated:: 8.13
+
+      Use :cmd:`Unshelve` instead.
+
 Proof modes
 ```````````
 
-- 
cgit v1.2.3