The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 01/02/2017 18:56, Andrew Harris wrote:
> Hi,
> 
>    I'm having some trouble understanding the ltac semantics of the Ltac
> invocation below (in the first email I sent (accidentally) below).  I've
> been reading Chapter 9 of the Coq book on Ltac, but what puzzles me is
> the square brackets around the rule in the "match goal with" section. 
> In chapter 9 of the book, there is a good section on "Pattern matching
> on goals", but it does not show square brackets in the expression and I
> am not able to figure out how the square brackets affect the
> expression.  It seems that when I see Ltac invocations with "match goal
> with" I always see the patterns surrounded by square brackets, and I'm
> not sure why.

These square brackets play no role; just ignore them. Perhaps they were
introduced for solving some cases where a pattern rule could not be
expressed due to some grammar ambiguity.

Best regards,

Guillaume