The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/17/2016 01:13 PM, Paul A. Steckler wrote:
> We might be able to do one or more of these, and we should discuss
> when I'm farther along.
>
> The XML protocol returns lists of goals, classified in various ways
> (shelved, abandoned, background). The window size can be queried, so
> the way goals are displayed can be cued from that.
>
> What types of hypotheses would you like to hide, or would you want
> that configurable in some way?
>
> -- Paul

Certainly configurable.  In some cases, showing hyps that other hyps or 
the conclusion depend on is redundant, because it is trivial for the 
user to figure out their types from their uses.  Maybe if those hyps 
were just highlighted at their uses in some way - maybe a particular 
color to indicate that they are hyps and not global constants.

However, because humans tend not to be as proficient at type inference 
as machines, there's probably some complexity such that merely 
highlighting a hyp at its usage and not dedicating a line to directly 
showing its type is annoying.  Maybe by having the mouse hover over the 
user click on a usage, that would bring up a tooltip with its type.  And 
clicking on the usage would make the line for that hyp visible.

Maybe that tooltip could apply to evars as well.  And maybe clicking on 
an evar would show its goal.



On a different front: how about a version of that new colorized progress 
bar that CoqIDE has at the bottom?

-- Jonathan