The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi, Gert,

I'm not sure if this will answer your question, but ssreflect comes
with a set of handy goal selectors. You can check in the reference
manual, section "Control Flow":
http://hal.inria.fr/inria-00258384

Best,
Beta

On Tue, Nov 15, 2011 at 10:22 AM, Gert Smolka 
<smolka AT ps.uni-saarland.de>
 wrote:
> Can I switch Coq's subgoal display in a mode where it shows only the 
> current subgoal?  The command Focus does it, but I have to reenter "Focus" 
> whenever I switch do a new goal, and I don't want to write "Focus" in my 
> scripts.  I'm working with Proof General.
>