The Coq mailing list

["Robert R. Schneck" <schneck AT math.berkeley.edu>]

I wanted to bring attention to the command "Focus 2." (or 1,3,etc) used to
focus attention on a particular subgoal while proving.  I stumbled upon it
by accident, it doesn't seem to be in the manual.  I think it should be, I
now use it all the time!

I like about this command that it retains the tree structure of the proof.
If you focus on a particular subgoal, and then apply a tactic that
generates several subgoals, you will see all of them.  Then you can focus
further if you wish.  Unfortunately Unfocus (or proving a subtree) will
unfocus completely, rather than just undoing the previous Focus n.

This use of Focus/Unfocus seems mostly independent of the documented use
to hide all but the first subgoal, except that Unfocus undoes both kinds
of focussing.

It might be helpful if subgoals could be labeled according to the tree
structure, e.g. if subgoal 2 is split into 3 subgoals, they are then 2.1,
2.2, and 2.3, and so forth.  Probably that I need such a feature just
shows that I need to use more lemmas.

Best,
Robert