coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Suggestions for Proof General?

From: "John Wiegley" <johnw AT newartisans.com>
To: Jonathan Leivent <jonikelee AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Fri, 17 Jun 2016 16:02:43 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f172.google.com
Ironport-phdr: 9a23:ogZEDxQBBlpN95k5Hxh0mjgEp9psv+yvbD5Q0YIujvd0So/mwa64YhSN2/xhgRfzUJnB7Loc0qyN4/GmCDVLuMjJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviqtuCOk4R2nKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6Ntb7teBSgmOmZ9wMDqqxTFUUPb5HwaU2YblhdFKwfA5RD+GJz2t32pmPB63XzQH8r2S/gLWDmt66p6Ale8iiAHMSER9mzIg9ZsjblSpgnnrBt6ld2HKLqJPeZzK/uONegRQnBMC55c
Organization: New Artisans LLC

>>>>> Jonathan Leivent
>>>>> <jonikelee AT gmail.com>
>>>>> writes:

> Could PG be made to show multiple complete goals if the goal window is big
> enough?

I'd like it if I could just always make sure that the top of the current goal
is brought into view after each command. I find myself manually scrolling the
response window often when large goals are involved.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

Re: [Coq-Club] Suggestions for Proof General?, (continued)