The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Ah, I see what you mean; thanks! I seems that I misread John's suggestion. 
This would indeed be a very nice (and relatively easy, I think) improvement 
to `coq-show-first-goal` in coq/coq.el.

Amusingly, I think Jonathan's specs are incomplete; what you describe does 
fullfil 1 + 3, since 4 + 6 it doesn't say anything about what to do when the 
first goal itself doesn't fit.

Clément.

On 2016-06-17 23:44, Jason Gross wrote:
> 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
>  
> <mailto: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)
>

Attachment: signature.asc
Description: OpenPGP digital signature