The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

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/

On Sat, Jun 7, 2014 at 12:17 PM, Jonathan <jonikelee AT gmail.com> wrote:

When dealing with goals having more hypotheses than can fit on the screen at once, is there an alternative to Set Hyps Limit that tries not to hide "useful" hypotheses?  I know that "useful" is a very subject term here, but just about any interpretation would be helpful.  Otherwise, I have the following proposal: If there is a set of hypotheses in a goal of exactly the same type, have a mode where they are all placed on the same line (subject to line length setting restrictions).  For example, a goal like:

    a : T
    b : T
    c : T
    d : T
    ...
    ====
    foo a b c d ...

would get displayed instead as:

    a b c d : T
    ...
    ====
    foo a b c d ...

as long as all of those T's are really the same type (i.e.: not different due to implicit args).

-- Jonathan