coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Alternative to Set Hyps Limit
- Date: Sat, 07 Jun 2014 15:28:34 -0400
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
- [Coq-Club] Alternative to Set Hyps Limit, Jonathan, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Pierre-Marie Pédrot, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Jonathan, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Abhishek Anand, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Jonathan, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Pierre Courtieu, 06/09/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Jonathan, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Pierre-Marie Pédrot, 06/07/2014
Archive powered by MHonArc 2.6.18.