The Coq mailing list

[Andrew Harris <andrew.unit AT gmail.com>]

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.

thanks,

-andrew

On Wed, Feb 1, 2017 at 9:50 AM, Andrew Harris <andrew.unit AT gmail.com> wrote:

Hi,



    Ltac t :=
    repeat (match goal with
              | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>
                dep_destruct E
            end; crush).