Shorten proofmode error messages and test them
Coq prints the body of locally bound functions but not of Ltac name := ...
-bound functions, so bind some more of them to shorten the error messages.
Also, change test harness to capture output of Fail ...
so we can test for #198 (closed) not to come back.