Stream: Coq users

Topic: assert (H := prf) deprecated


view this post on Zulip Dan Frumin (Aug 09 2023 at 11:40):

My Emacs/Proof General complains that the tactic form assert (H := prf) is deprecated since 8.5, but I didn't manage to find anything about that in the reference manual. What is the preferred way of asserting particular terms? I use assert because I want it to be "opaque" during the proof, so IIUC pose is not an alternative

view this post on Zulip Janno (Aug 09 2023 at 11:49):

pose proof exists but I am not sure if that is the recommended alternative

view this post on Zulip Gaëtan Gilbert (Aug 09 2023 at 11:49):

you can use pose proof prf as H or pose proof (H := prf)
not sure the assert (H := prf) is actually deprecated though

view this post on Zulip Paolo Giarrusso (Aug 09 2023 at 13:22):

Does coqc report a deprecation? What's the actual message?

view this post on Zulip Gaëtan Gilbert (Aug 09 2023 at 13:23):

no, only pg

view this post on Zulip Karl Palmskog (Aug 09 2023 at 13:24):

then please report as PG bug: https://github.com/ProofGeneral/PG/issues

view this post on Zulip Gaëtan Gilbert (Aug 09 2023 at 13:26):

actually company-coq not pg

view this post on Zulip Karl Palmskog (Aug 09 2023 at 13:29):

https://github.com/cpitclaudel/company-coq/issues

view this post on Zulip Théo Zimmermann (Aug 11 2023 at 16:28):

IIRC assert := used to be deprecated in the Coq refman too, but it has been undeprecated for many years


Last updated: Jun 23 2024 at 05:02 UTC