diff options
| author | Maxime Dénès | 2020-06-15 17:22:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-16 12:00:05 +0100 |
| commit | e348b1b6761315cdeea9e4c1c2f610ace9787e4a (patch) | |
| tree | 02915e1af8db0716afa876657a51d98bc11e7209 /proofs/proof.ml | |
| parent | a118b906b3da7cb2e03a72f7a8079a7fc99c6f84 (diff) | |
Deprecate `Grab Existential Variables` and `Existential` commands
Diffstat (limited to 'proofs/proof.ml')
| -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) = |