The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Sean Wilson wrote:

> I wish to write a Coq tactic that matches goals that are similar to that of 
> the following statement:
>
> Definition test : (let (a,b) := (0, 1) in a=0).
>
>  
Compound lets aren't compiled into real lets.  Try this instead:

Ltac letPair :=
match goal with
 | [ |- context[ match _ with (_, _) => _ end ] ] => idtac
end.

> Also, how would I go about outputting matched patterns in Ltac for debug 
> purposes?
To make available expression E for perusal, you can do something like 
"assert (E = E)" in your tactic.  Pretty hackish, but I don't know a 
better way.