The Coq mailing list

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

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>:

>>>>> Pierre Courtieu <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