Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Definitions for Parsing Compatibility

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Definitions for Parsing Compatibility


Chronological Thread 
  • From: scott constable <sdconsta AT syr.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Definitions for Parsing Compatibility
  • Date: Sat, 20 Feb 2016 10:22:46 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sdconsta AT syr.edu; spf=None smtp.mailfrom=sdconsta AT syr.edu; spf=None smtp.helo=postmaster AT smtp1.syr.edu
  • Ironport-phdr: 9a23:f2SO2hBd7skKJFQZkeMAUyQJP3N1i/DPJgcQr6AfoPdwSP74osbcNUDSrc9gkEXOFd2CrakU1KyL6eu+CCQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTokb3osMOCKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs2AXVXkK2hFPBRPZ5Rv+U9+lqSfxsexmxCCyJtzsC704RGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==

Thanks Pierre, this makes sense to me now.

~Scott

On Sat, Feb 20, 2016 at 5:04 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:
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






Archive powered by MHonArc 2.6.18.

Top of Page