The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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?


How about a real-time extraction window?  This was started, but not 
completed.  I think the last time I checked there were issues on the Coq 
side in that what it was sending was a non-optimized extraction - what 
the window showed was much larger/complex than what would be extracted 
via the Extraction command when the definition was finished.


-- Jonathan