tactics don't fail enough #7

TomHarke opened this Issue Aug 11, 2010 · 0 comments


None yet

1 participant


Tactics based on Hein's text don't fail when misused, instead the do nothing except report an error. It should fail outright. The reason for this no-op behavior is the way the tests of the tactics are written: one proof tests all possible modes of failure. A prerequisite for making tactics fail outright is that the tactic tests be expanded.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment