The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear Coq users,

I have some hypothesis with a match expressions with many branches in it. Now
I want to use an ltac match to match such a hypothesis. The problem is, that I
have to specify all branches of the match expression, but for me it would be
sufficient to specify the first branch only to instantiate the metavariables I
Need for the tactic. Is there a way in an ltac match to say ... for "+ any
additional branches"?

Something like

match goal with
  | H1: match ?a with | Empty => _ | ... end |- _ => destruct a
end.

at the ... the hypothesis has additional branches, which I don't want to
specify in the tactic. For all other expressions I can use _ when I want to
leave something away, but I cannot get this to work with match branches.

Thanks & best regards,

Michael