The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I was hoping to avoid needing to run the preceding tactic twice, or even needing to know what it is.

On Fri, Jun 13, 2014 at 4:19 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

Just use an "||" composition of your two tactics, for "no goals left" and "exactly one goal left".  Admittedly, it's too bad to need to run the preceding tactic twice in some cases.

On 06/13/2014 11:16 AM, Jason Gross wrote:

Actually, my [at_most_one_goal_left] tactic doesn't work.  Is there a way to detect "zero or one goals"?

On Fri, Jun 13, 2014 at 4:11 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Hi,

Is there a standard way of asking the question "are all goals solved?" and "is there at most one goal left?" in Ltac?

I can use "; solve [ idtac ]" to mean "fail if there are any goals left", and I have been using "; []" to detect "exactly one goal left", and and I can define a tactic

  Ltac at_most_one_goal_left := idtac; [].

so that "; at_most_one_goal_left" will fail if there is more than one goal.  But is seems poor that inlining a tactic definition changes its behavior; am I simply exploiting a bug?

-Jason