The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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