The Coq mailing list

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

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.

P.

2016-06-23 17:54 GMT+02:00 Clément Pit--Claudel <clement.pit AT gmail.com>:

👏 Thanks Pierre!
Should we enable this by default?

On 2016-06-23 11:47, Pierre Courtieu wrote:
> Done in trunk.
>
> (setq coq-prefer-top-of-conclusion t)
>
> should do it.
>
> Best,
> P.
>
> 2016-06-23 17:04 GMT+02:00 John Wiegley <johnw AT newartisans.com <mailto:johnw AT newartisans.com>>:

>
>     >>>>> Pierre Courtieu <pierre.courtieu AT gmail.com <mailto:pierre.courtieu AT gmail.com>> writes:
>
>     > When the goal is large, PG displays as much as possible of the goal, with an
>     > order of precedence: - prefer conclusion over hyps (1) - prefer bottom of
>     > the conclusion over its top (2)
>     >
>     > This is rather empirical setting. (1) is hardly questionable imho, but (2)
>     > is indeed arbitrary. I can maybe have an option for (2).
>
>     An option for (2) would be very helpful. I'm working with MIT's Fiat system,
>     which involves proofs that refine monadic, non-deterministic blocks "action by
>     action", from top to bottom, so knowing the bottom of the conclusion without
>     seeing the top is relatively useless.
>
>     Thanks,
>     --
>     John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
>     http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2
>
>