Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Alternative to Set Hyps Limit

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Alternative to Set Hyps Limit


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page