The Coq mailing list

[Arnaud Spiwack <arnaud AT spiwack.net>]

Well, at_most_one_goal_left will always succeed in the current semantics (even all:at_most_one_goal_left). Also, solve[idtac] is equivalent to fail.

But I'm glad you are bringing that to the table. Because it is a sore point in Ltac's behaviour. Point to the matter: (a;b);[t1…tn] doesn't mean the same thing as a;(b;[t1…tn]). In the first case, [t1…tn] is applied to the n goals generated by a;b. But the latter tactic will apply [t1…tn] to the n goal generated by b, in each of the subgoals generated by a.

This is a real problem because: 1/ It probably cannot be changed (to much code rely on it) 2/ It'd be really sweet to change it, if only because I want to make a;[t1…tn] into the composition of a;   and [t1…tn]. So that the latter can be called as it's own bona fide tactic (with all: for instance).

That being said, independently of the matter of dispatched tactics (as I call them). It is easy to write a bunch of ML tactic, in trunk, which could count the number of focused goals. Using Proofview.Goal.goals or, more efficiently, by adding a primitive in Proofview (proofs/proofview.ml).

Arnaud

On 13 June 2014 17:11, 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