The Coq mailing list

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

Attachment: signature.asc
Description: OpenPGP digital signature