Failing test cases for tactics

[upamanyus]

Some tactics (e.g. wp_pures) try to give helpful error messages when they fail. This can be fragile, such as carefully picking the number 3 in fail 3 "some error message" to make sure that tactic execution backtracks to just the right level. Changes to higher-level tactics can break these useful error messages.

Having some tests in which some tactics fail (try wp_load in a proof in which it will fail and ensure it has the expected error output) would prevent regressions. The program proofs already serve as tests for successful applications of tactics.