The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

There is no such thing currently, but it is on my todo list. Actually
I plan to make the Coq messages about subgoals more explicit about the
nature of the "next" goal.

Best regads,

Pierre

2014-07-03 23:45 GMT+02:00 Jonathan 
<jonikelee AT gmail.com>:
> Does anyone know if there is command in PG to insert the "proper" bullet at
> a particular point in a proof script?  In long scripts, after closing out a
> subgoal, I have to guess - + * { or } until I get the right one, or go
> examine the indentations up the script .
>
> -- Jonathan
>