The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/24/2015 03:11 AM, Jason Gross wrote:
> Hi,
>
> In case others may find this discovery interesting (if you have not already
> made it yourselves):
> It is possible to mostly eliminate the verbose [match goal with ... end]
> construct in trunk/8.5 by using the following tactic:
>
>    Ltac hyp := multimatch goal with H : _ |- _ => constr:H end.
>
> Note that [let H := hyp in ... ] will automatically backtrack across
> failures of subsequent tactics, due to [multimatch]:
>
>    Goal False -> True -> False -> True.
>      intros.
>      let H := hyp in exact H.
>
> Using open_constr and uconstr tactic notations, I presume the other
> features of match (pattern matching on the body and the type) can be
> duplicated with shorter syntax, too.
>
> -Jason

I wasn't able to duplicate the match feature of named pattern variables 
with any combo of open_constr and uconstr, at least not without using 
evars in their place (which is not as good as one can easily leave 
unsolved evars as a result).

Which is one reason why I was asking you about those other Tactic arg 
notations that are undocumented.

-- Jonathan