idris-lang/Idris-dev — pull request #726 by Melvar (2013-12-12 19:15:55+00:00)
Title: Fix too-new import

fixes https://github.com/idris-lang/Idris-dev/issues/724