Stream: Coq users

Topic: Are Local/Global deprecated?


view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 22:25):

https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#controlling-the-locality-of-commands

There is also a legacy (and much more commonly used) syntax using the Local or Global prefixes (see legacy_attr).

Is the legacy syntax also scheduled for removal?

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 22:26):

I have no real argument against, but I'm sticking to the old one out of aesthetic reasons, and a colleague would prefer switching to the new one....

view this post on Zulip Théo Zimmermann (Nov 04 2020 at 09:59):

No @Paolo Giarrusso, the legacy attribute syntax is not scheduled for removal (at least for now). At the moment, the important difference is that new attributes will only be provided using the new mechanism and the legacy attributes won't be extended.

view this post on Zulip Théo Zimmermann (Nov 04 2020 at 10:00):

Maybe we should write that down in the refman.


Last updated: Feb 08 2023 at 23:03 UTC