coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Fri, 17 Jun 2016 22:26:26 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:Vn0KtROmoUgOhpPCOtEl6mtUPXoX/o7sNwtQ0KIMzox0KPj+rarrMEGX3/hxlliBBdydsKIVzbuP+P65EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35Xxhrn5pcSbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7azX+dV2gQji1wAhSAqTr+V4r9vy+y4uF51SyXO9GwVbEocTun5qZvDhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==

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)

Attachment: signature.asc
Description: OpenPGP digital signature

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