Ali Caglayan (Oct 05 2021 at 09:55): 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
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?
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
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: Oct 13 2024 at 01:02 UTC