Stream: Coq users

Topic: `intropattern` has been renamed


view this post on Zulip Ali Caglayan (Oct 05 2021 at 09:55):

I'm trying to use intropattern in a tactic notation however I get this warning:

Entry name intropattern has been renamed in order to be consistent with the
documented grammar of tactics. Use "simple_intropattern" instead.
[deprecated-intropattern-entry,deprecated]

But the refman says that intropattern ::= * | ** | simple_intropattern. How else can I use *? This is all 8.15+alpha

view this post on Zulip Paolo Giarrusso (Oct 05 2021 at 09:59):

https://coq.github.io/doc/master/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation might imply you can't?

view this post on Zulip Paolo Giarrusso (Oct 05 2021 at 10:00):

Except maybe with ssr analogues: I've seen people reuse ssr nonterminals in tactic notations, it seemed to work just fine

view this post on Zulip Théo Zimmermann (Oct 05 2021 at 10:00):

What this means is that intropattern in a tactic notation doesn't match the intropattern grammar, and we have to deprecate the current one before introducing a new one that would match.


Last updated: Feb 06 2023 at 12:04 UTC