Better parsing error recovery for bad parsing inside a proof.

[ejgallego]

We want to handle this case:

Proof.
tac1, tacn
Qed.

Better, so we just don't skip to dot, but can detect the Qed and be smarter here.

Note the lack of doc after tacn