The Coq mailing list

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

Hello coq-club,

here is a little poll for you about the inclusion details of a feature
in Coq 8.6. From this version, it will be possible to use first-class
quotations in Ltac that were previously limited to Tactic Notations, e.g.

let id := ident:(foo) in ...

let c := open_constr:(f _ _) in ...

The string in parentheses is parsed as the argument described by the
string and then interpreted as such.

For uniformity and parsing reasons, the current implementation requires
such quotations to be of the form IDENT COLON LEFTPAREN entry
RIGHTPAREN, with mandatory parentheses.

Pro:

1. Uniform quotation syntax, as used by most (meta-)languages
2. Allowance of parsing of objects where spaces are significant, e.g.
complex intro-patterns of the form "[] []"

Cons:

1. No more special handling of the constr:(...) entry.

This means that constr quotations require parentheses as well, and that
you cannot write

constr:x

anymore. Likewise, for reasons I am not really sure to understand, it
forces you to write the ugly

constr:((x, y))

when parsing pairs. The proeminence of terms in Ltac was the reasons why
such a special case was introduced, to save the user of a potentially
repeated two-character burden.

Note that it is easy to provide forward compatibility between 8.5 and
8.6, by simply adding an additional pair of parentheses around the
argument. E.g., the above case should be written constr:(x) to be both
8.5 and 8.6 compatible.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
QUESTION

What do you believe? Should we still special case constr entries or
should we aim at uniformity? Is the translation of your developments
going to be painful?
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Thanks for your attention,
PMP

Attachment: signature.asc
Description: OpenPGP digital signature