Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Alternative to Set Hyps Limit


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Alternative to Set Hyps Limit
  • Date: Sat, 07 Jun 2014 12:17:15 -0400

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




Archive powered by MHonArc 2.6.18.

Top of Page