The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Hi,

Something like:

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

should work.

--
JH Jourdan




Le 27/06/2014 03:55, 
michael.soegtrop AT intel.com
 a écrit :
> 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