The Coq mailing list

[Andrew Hirsch <akhirsch AT gwmail.gwu.edu>]

I've been playing with some Ltac recently, but I've not been able to get Coq to except it: when I try this piece of Ltac from Adam Chilpala's book, I get this error:

Code:

Ltac my_tauto :=

  repeat match goal with

           | [ H : ?P |- ?P ] => exact H

           | [ |- True ] => constructor

           | [ |- _ /\ _ ] => constructor

           | [ |- _ -> _ ] => intro

           | [ H : False |- _ ] => destruct H

           | [ H : _ /\ _ |- _ ] => destruct H

           | [ H : _ \/ _ |- _ ] => destruct H

           | [ H1 : ?P -> ?Q, H2 : ?P |- _ ] => specialize (H1 H2)

         end.

Error:

Toplevel input, characters 90-91:

Syntax error: ',' or '|-' expected (in [match_context_rule]).

Which is right over the first closing bracket.

It works fine if I don't try to match hypotheses, but the moment I do, I get this error.

Any ideas?

-Andrew