The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/13/2014 11:46 AM, Arnaud Spiwack wrote:
> ...
> Goal counting is easy. Of course, since Ltac doesn't have datatype, we'll
> need to make special tactics and syntax for most use case. Do you have any
> opinion on the design?

If goal counting was implemented, which goals would it count?  Would it 
count all outstanding goals? Or would it only count subgoals generated 
by the previous tactic?  Would it count shelved goals? Unsolved 
existentials?

If Jason's usage for "at most one goal left" applies to the current goal 
subtree where the tactic is being called and not to other subtrees, you 
would need goal counting to be similarly restricted to be helpful in 
that case.