The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/23/2016 04:37 PM, Ralf Jung wrote:
> Hi,
>
> On 23.06.2016 22:27, Pierre Courtieu wrote:
> > I don't know, I think most of regular users's large goals are of the form
> > ...
> > ======
> > P1 ->
> > P2 ->
> > ...
> >
> > Pn ->
> > P
> >
> > and in this case isn't P what people want to see?
> > Well... At least ssreflect users may want this option set by defaut
> > since P1 is the "active" hypothesis.
> We frequently have goals where "P" is large. Usually that's an accident
> ;-)  but for example, proving a Hoare triple about an interesting piece
> of code can result in a pretty long goal of which only the beginning
> (the expression in head position) is interesting. We are not using the
> ssreflect proof style, and I can hardly imagine a case where we'd prefer
> to see the end of the goal over its beginning.
> So, I'd personally set coq-prefer-top-of-conclusion to t (thanks for
> adding that!).
>
> Kind regards,
> Ralf

In a really long telescope, would it make sense to be able to see the 
beginning and the end, with the middle initially hidden?
Maybe another opportunity for hide-show?  So that the goal would look 
like this initially:

======
P1 -> ... P

with the ability to show more info on the left by clicking?

-- Jonathan