The Coq mailing list

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

Hi, notice that the number of goal is aldready displayed in the
modeline of the scripting buffer (next to "Coq script").  Notice
however that in coq 8.4 the number displayed is more of a list of
numbers corresponding to the focus levels.

The lisp code to do that is quite hackish in pg (see coq.el around
line 2630) but it should be easy to make this appear also in the
modeline of the goals buffer. Let me know if the current display is
not satisfying for you.

Best REsgards,
Pierre Courtieu

2012/9/12 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