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

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

1 files changed, 14 insertions, 0 deletions

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