The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/17/2016 01:38 PM, Paul A. Steckler wrote:
> ...
>
> OK, I think these requests should keep me busy!
>
> -- Paul

But wait!  There's more! :-)

On the topic of trying to keep the goals window showing all and just 
what the user wants: how about a context-dependent Print Depth?  For 
example, in local defs, which sometimes tend to be large, maybe have the 
value hidden until tooltip'ed or clicked on.  Or a different print depth 
for hyps vs. the conclusion.  Or maybe just a general a way to hide/show 
subterms, with settable defaults (like always initially hide a local 
def's value, initially hide below depth 3 in hyps, etc.).

But, maybe this set of suggestions is really more for Company Coq than 
PG...  Like that suggestion of fireworks and music on a successful proof 
(I'm sure Clément gave that more than just a passing thought ;-)).

-- Jonathan