The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

That is indeed possible to hack a hook for that, consider this in my
todo list in PG. As I am quite busy lately I cannot code this before
late summer I guess. Anyone willing to do this can try to hack
proof-shell-handle-delayed-output-hook. See for examples: coq.el
around line 2150.

This can also be added as an option to coq output. I don't know how it
would fit in the new ide/coq protocol in trunk.

Best regards,
P.

2014-06-07 21:28 GMT+02:00 Jonathan 
<jonikelee AT gmail.com>:
> On 06/07/2014 12:55 PM, Abhishek Anand wrote:
>>
>> I already do this in my editor.
>> https://www.youtube.com/watch?v=94D5RVK-cQg#t=297
>> In practice, I found this bunching to hypothesis of same type to be quite
>> useful.
>> Note that coqtop already provides
>> the information required to produce such a display of proof state.
>> So, you might want to send this request to the developers of your Coq
>> editor/IDE.
>>
>> -- Abhishek
>> http://www.cs.cornell.edu/~aa755/
>
>
> Unfortunately, I have to use a more recent version of Coq than 8.4pl2 in my
> current developments (a trunk version that has full backtracking over evars
> via typeclasses eauto and the "+" Ltac operator) - so I can't use your nbcoq
> plugin.
>
> But, if coqtop makes the info available, then there should be a way to get
> Proof General to do this.  Unfortunately, I am not a proficient emacs
> hacker.  And the developers of PG seem to be more focused these days on
> other things.
>
> But if this is a common request, as others have suggested, maybe someone
> knows of an existing way to get Proof General to do it?
>
> -- Jonathan
>