idris-lang/Idris-dev — pull request #1658 by david-christiansen (2014-10-18 18:32:21+00:00)
Title: Removal of minor TODOs

Some were completed before and we forgot to remove the TODO, while
others I just took care of.