coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Variant of [try] that says "it must succeed somewhere"?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Variant of [try] that says "it must succeed somewhere"?
Date: Mon, 30 Jul 2012 22:45:13 -0400

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

[Coq-Club] Variant of [try] that says "it must succeed somewhere"?, Jason Gross, 07/31/2012
- Re: [Coq-Club] Variant of [try] that says "it must succeed somewhere"?, Gregory Malecha, 07/31/2012