The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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