Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Displaying the number of goals in the modeline in Proof General

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Displaying the number of goals in the modeline in Proof General


Chronological Thread 
  • From: Alan Schmitt <alan.schmitt AT polytechnique.org>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Displaying the number of goals in the modeline in Proof General
  • Date: Wed, 12 Sep 2012 11:12:06 +0200

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



Archive powered by MHonArc 2.6.18.

Top of Page