The Coq mailing list

[t x <txrev319 AT gmail.com>]

This worked, thanks. I'm starting to see how fail / backtrack interact.

On Tue, Jul 9, 2013 at 1:31 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 07/09/2013 04:29 PM, t x wrote:

I want to write a ltac that says: "apply this lemma, if and only if the newly introduced goals can be solved by omega"

Perhaps [apply lemma; solve [ omega ] ]?