From e348b1b6761315cdeea9e4c1c2f610ace9787e4a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 15 Jun 2020 17:22:23 +0200
Subject: Deprecate `Grab Existential Variables` and `Existential` commands

---
 proofs/proof.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/proofs/proof.ml b/proofs/proof.ml
index d864aed25a..24f3ac3f29 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -409,14 +409,28 @@ module V82 = struct
   let top_evars p =
     Proofview.V82.top_evars p.entry p.proofview
 
+  let warn_deprecated_grab_existentials =
+    CWarnings.create ~name:"deprecated-grab-existentials" ~category:"deprecated"
+       Pp.(fun () -> str "The Grab Existential Variables command is " ++
+         str"deprecated. Please use the Unshelve command or the unshelve tactical " ++
+         str"instead.")
+
   let grab_evars p =
+    warn_deprecated_grab_existentials ();
     if not (is_done p) then
       raise (OpenProof(None, UnfinishedProof))
     else
       { p with proofview = Proofview.V82.grab p.proofview }
 
+  let warn_deprecated_existential =
+    CWarnings.create ~name:"deprecated-existential" ~category:"deprecated"
+       Pp.(fun () -> str "The Existential command is " ++
+         str"deprecated. Please use the Unshelve command or the unshelve " ++
+         str"tactical, and the instantiate tactic instead.")
+
   (* Main component of vernac command Existential *)
   let instantiate_evar env n intern pr =
+    warn_deprecated_existential ();
     let tac =
       Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
       let (evk, evi) =
-- 
cgit v1.2.3


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.

---
 .../07-commands-and-options/12516-deprecate-grab-existentials.rst   | 4 ++++
 doc/sphinx/proofs/writing-proofs/proof-mode.rst                     | 6 ++++++
 2 files changed, 10 insertions(+)
 create mode 100644 doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst

diff --git a/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst b/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst
new file mode 100644
index 0000000000..1c7c3102a3
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst
@@ -0,0 +1,4 @@
+- **Deprecated:**
+  :cmd:`Grab Existential Variables` and :cmd:`Existential` commands
+  (`#12516 <https://github.com/coq/coq/pull/12516>`_,
+  by Maxime Dénès).
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