Merge PR #12516: Deprecate `Grab Existential Variables` and `Existential` commands

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

3 files changed, 24 insertions, 0 deletions

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
 ```````````
 
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) =