Skip to content

Shorten proofmode error messages and test them

Ralf Jung requested to merge ralf/reftests into gen_proofmode

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.

Edited by Ralf Jung

Merge request reports