idris-lang/Idris-dev — pull request #1425 by david-christiansen (2014-07-24 21:28:31+00:00)
Title: Add tactics "skip" and "fail"

"skip" does nothing, while "fail" produces an error. They have
corresponding reflected versions Skip and Fail. Fail has access to the
pretty printer by taking a List ErrorReportPart as its argument.