The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

Hi,

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).

I've tried the following tactic when a proof of the above statement is 
started:

Ltac m1 :=
match goal with
| |- context [let _ := _ in _] => idtac "Match!"
end.

And it fails to match. However, it matches goals of the form "(let a := 0 in 
a=0)". I then tried:

Ltac m2 :=
match goal with
| |- context [let (_,_) := _ in _] => idtac "Match!"
end.

Coqide replies "User error: Not supported pattern" for the pattern with the 
let expression containing the pair. How can I write a tactic that matches 
goals of this form?

Also, how would I go about outputting matched patterns in Ltac for debug 
purposes? For example, given the following:

Ltac m3 :=
match goal with
| |- context [let _ := _ in ?X] => idtac X
end.

I would like this to output what X was matched with but idtac wants a string 
as input.

Thanks,

Sean