coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] focus on current goal

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] focus on current goal
Date: Tue, 15 Nov 2011 10:22:24 +0100

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.

[Coq-Club] focus on current goal, Gert Smolka
- Re: [Coq-Club] focus on current goal, Beta Ziliani
- <Possible follow-ups>
- Re: [Coq-Club] focus on current goal, Pierre Boutillier
- Re: [Coq-Club] focus on current goal, Gert Smolka