coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]suppress printing on display

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]suppress printing on display
Date: Wed, 16 Aug 2006 13:35:35 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, 16 Aug 2006 13:44:50 +0900 (JST) Keiko Nakata
<keiko AT kurims.kyoto-u.ac.jp>
wrote:
> Hello,
>
> How can I stop Coq from printing subgoals other than the current one on
> display?
> What I only know is to use "Set Printing Depth",
> which is not very good for this purpose.
>
> Best regards,
> Keiko.

You can use "Focus."

Focus n. focuses on the nth goal.

Unfocus to leave this mode.

Cheers,
P.C.

[Coq-Club]suppress printing on display, Keiko Nakata
- Re: [Coq-Club]suppress printing on display, Pierre Courtieu