The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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

Attachment: signature.asc
Description: OpenPGP digital signature