coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Sat, 18 Jun 2016 03:44:19 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f52.google.com
Ironport-phdr: 9a23:iO0BeBTkr9iNRQ9lRtw+0aZdGNpsv+yvbD5Q0YIujvd0So/mwa64ZxKN2/xhgRfzUJnB7Loc0qyN4/GmCDVLvs3JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviqtuCOk4X33KUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzA0mwFPBUDq9hbhRd+lsCLhsexywi6BJpzeQrU9WDDk5KBuHky7wBwbPiI0pTmEwvd7i7hW9Uqs

If it's a bug, then it's systematic; my experience is that PG aligns the bottom of the goals window with the bottom of the first goal, rather than preferring to align with the top when the goal is too big to fit in the buffer.

On Fri, Jun 17, 2016, 7:26 PM Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

On 2016-06-17 19:26, Jonathan Leivent wrote:
> Here's a priority order of what I'd like to see without scrolling, if the goal window is big enough:
> 1. all of the goals in focus, with their hyps
> 2. all of the current goal, and as many of the next goals as can fit completely, but at least all conclusions
> 3. the whole current goal's conclusion, with as many hyps above it as fit

I think 1 + 3 is the current behaviour (IIRC)

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