The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/07/2014 12:51 PM, Pierre-Marie Pédrot wrote:
> On 07/06/2014 18:17, Jonathan 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).
> This is a recurring wish. What interface are you using?
>
> PMP

Proof General, Version 4.3pre131011

However, if there is a way to do this in coqide, I'd be willing to switch.

-- Jonathan