idris-lang/Idris-dev — pull request #1498 by david-christiansen (2014-08-30 18:55:35+00:00)
Title: Error when using empty namespace for disambiguation at REPL

Fixes #1497.