diff options
| -rw-r--r-- | proofs/proof.ml | 14 |
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) = |