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
https://coq.github.io/doc/master/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation might imply you can't?
Except maybe with ssr analogues: I've seen people reuse ssr nonterminals in tactic notations, it seemed to work just fine
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: Sep 23 2023 at 14:01 UTC