The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hi, Jason --

This probably isn't quite what you want, but if [tac] is meant to solve the goal (like [assumption]) then you can do something like:

(etransitivity; try tac); [] 

The [ ] enforces that there is exactly 1 goal after the parenthesized tactic finishes. This is the best that I've been able to do with goals like this, but the approach can be useful in other instances as well. 

On Mon, Jul 30, 2012 at 10:45 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Hi,

I was wondering if there's a variant of [try tac] that fails if tac doesn't succeed on any goal.  For example, I want this tactic to fail on [etransitivity; progress-try tac] if tac fails on both of the two branches, but I want it to succeed if tac succeeds on either or both of the branches.  I've tried [progress try], and that doesn't do what I want...

Thanks.

-Jason

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/