The Coq mailing list

[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