The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

How about:

idtac; [idtac|fail..].

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