The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 17/02/2016 22:51, scott constable wrote:
> What exactly is the purpose of reintroducing existing tactics as
> identical notations?

AFAIK, that's purely a parsing issue.

Since Coq 8.5, some tactics defined in ML are registered as true Ltac as
they do not require parsing rules. Typically, tactics whose grammar is
of the form

"ident" constr₁ ... constrₙ

for any n. Alas, this clashes with some other notations that are indeed
changing the parsing rules. For instance, in the list you mentionned,
"constructor" has a variant "constructor" integer(i). This leads to
various issues that prevent parsing "constructor" alone.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature