The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 2016-06-17 12:47, Jonathan Leivent wrote:
> Could PG be made to show multiple complete goals if the goal window
> is big enough?  I know there are various ways to ask for one or more
> goals to be shown, but this question is whether it is possible to do
> this automatically based on the size of the goal window.
> 
> How about having a separate goal window for the current goal vs for
> the others?
> 
> How about having a way to automatically show non-focused goals, as
> via Show Existentials, in a separate window?
> 
> How about having a way to hide hypotheses based on type, or based on
> their being depended on in other hyps?  True - the current
> multiple-hyps-per-line is very nice, but it would be really nice if
> what I see in the goals window is just what I need to see (subject to
> choices) and room is not taken up by unimportant or redundant info.
> Set Hyps Limit isn't discriminating.  Maybe have the goal window just
> show some tool-tip-able small icon to show where some invisible hyps
> are in the context?

Cool list! Thanks. We should try separating this into features that PG can 
have without specific support from Coq vs other features. Could you open 
tickets on PG's github?

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature