The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

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