The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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