The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

The original split is not an ltac definition. It is recognized by parsing rule but it does not have a corresponding ltac entry. Therefore if you define a notation with split it will not combine with it, it will hide the original one.

Pierre

Le jeudi 18 février 2016, scott constable <sdconsta AT syr.edu> a écrit :

Thanks for the responses. I think I understand the problem somewhat, but let me try to make it more concrete. Suppose that I want to define two kinds of split, "split~" for chaining auto after split, and "split*" for chaining tauto after split. So I might do this:

Tactic Notation "split" "~" :=

  split; auto.

Tactic Notation "split" "*" :=

  split; tauto.

But Coq rejects the second notation with the error: "Syntax error: '~' or 'with' expected after 'split' (in [tactic:simple_tactic])." Yet when I instead use

Tactic Notation "split" :=

  split.

Tactic Notation "split" "~" :=

  split; auto.

Tactic Notation "split" "*" :=

  split; tauto.

I no longer get the error. Could someone please explain in the context of this example what went wrong in the first case, and how the second case resolved the issue?

Thanks again,

~Scott

On Thu, Feb 18, 2016 at 5:17 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

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