The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

Gert Smolka 
<smolka AT ps.uni-saarland.de>
 writes:

   Can I switch Coq's subgoal display in a mode where it shows
   only the current subgoal? 

I just noticed yesterday that Proof General provides the
necessary infrastructure for years already: proof-shell-end-goals-regexp

There were however two problems. First, Proof General leaves the
*goals* buffer empty, when proof-shell-end-goals-regexp was set
but did not match. Second, when it matched, Proof General showed
everything including the match.

Because occasionally I also had the wish to hide the subgoal
noise, I fixed those things and added an entry "Hide Additional
Subgoals" in the Coq->Settings menu. You'll find all that in the
latest cvs development version of Proof General.

Bye,

Hendrik Tews