The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/31/2016 11:05 AM, Pierre-Marie Pédrot wrote:
> 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 "[] []"

This looks really good...

Will it be possible to use Ltac to incrementally build up and break down 
things like simple_intropattern and hyp_list?  Or will they stay opaque 
as in 8.5?

> 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.

I did some grepping and found I have only one instance of constr: 
lacking parens - and that is:

Ltac last_hyp := lazymatch goal with H : _ |- _ => constr:H end.

In this case, the "constr:" isn't needed in 8.5.  Will that change in 
8.6?  In other words, will it be necessary to enclose all constrs in a 
"constr:(...)" wrapper in 8.6, even those not requiring this in 8.5?  It 
will be harder to find such occurrences...

-- Jonathan