The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2016-06-23 22:37 GMT+02:00 Ra.

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.

You are of the "strongest postcondition" chapel then. And Thou shall Burn in Hell for such perverted practice! :-)

Seriously I have no clue what default setting would satisfy the most users. Not mentioning the hundreds of other questionable default settings in pg..

 

P.

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