assert command etc.: strange movement of point

[Makarius]

GNU Emacs 23.1.1, Mac OS.

The point movement after asserting commands is still a bit odd. With proof-assert-next-command there is a higher change that it moves after the span than with proof-goto-point, where it seems to move to the span start unconditionally. But there are situations where both fail.

Also note that proof-goto-point does not work if the point is at the first position of the command keyword.

[David Aspinall]

Known, but thanks. See #278