The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/05/2014 09:28 AM, Pierre Courtieu wrote:
> 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

By any chance are the Coq developers' todo lists public?  I'd probably 
(no promises) be less of a nuisance if I could see them.

-- Jonathan

> 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