H1 : {a, b, c, d, e, [F] |- X}
H2 : member F (e :: d :: c :: b :: a :: nil)
instead of one case for each member of the context. This is really annoying if the contexts have more than a few elements. Matteo ran into subgoals with numbers like 3.2.2.2.1.2.1.2.2.1.2.1 (not kidding).
The object-case-tweaks branch (commits starting with 96fce26514b) fixes this issue, but it breaks too many existing proofs. I have therefore backed it out of master and am postponing it to the 2.1 milestone.
Matteo Cimini pointed out this issue.
When we have a hypothesis such as
and do a
case H, it produces:instead of one case for each member of the context. This is really annoying if the contexts have more than a few elements. Matteo ran into subgoals with numbers like
3.2.2.2.1.2.1.2.2.1.2.1(not kidding).The object-case-tweaks branch (commits starting with 96fce26514b) fixes this issue, but it breaks too many existing proofs. I have therefore backed it out of master and am postponing it to the 2.1 milestone.