The Coq mailing list

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

Pierre Courtieu 
<pierre.courtieu AT gmail.com>
 writes:

> 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.

I had not noticed this. Thanks a lot for pointing it out.

> 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.

No, it's fine. I was just looking at the wrong place.

Thanks again,

Alan