coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] match goal with context

From: Adam Chlipala <adam AT chlipala.net>
To: Michael Shulman <mshulman AT ucsd.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] match goal with context
Date: Fri, 22 Apr 2011 15:55:25 -0400

Michael Shulman wrote:

Ltac test :=
   match goal with
     context cxt [S ?X] =>  idtac X
   end.

You're just missing "|-" at the start of the 3rd line. Context patterns are alternatives to normal top-level expression patterns, and they must be used in the same way. E.g., your example wouldn't work either if you removed the context stuff without also adding the turnstile.

[Coq-Club] match goal with context, Michael Shulman
- Re: [Coq-Club] match goal with context, Adam Chlipala