The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

Hello,

I've been searching the web and mailing list archives yet could not find
a way to do the following: display the number of goals in the modeline
of the *goals* Proof General buffer. It can be quite handy when there
are many goals or when they are very big.

Any suggestion as how to do this?

Thanks a lot,

Alan