idris-lang/Idris-dev — pull request #1145 by raichoo (2014-05-01 10:06:09+00:00)
Title: Fix #1015

Issuing 'undo' in the prover when there is
nothing to undo should result in a less
scary looking error message.