idris-lang/Idris-dev — pull request #1773 by JakobBruenker (2014-12-07 01:44:53+00:00)
Title: Added ":refine" to the autocompletions in the REPL

More specifically: added ":refine", ":ref", "refine!" and "ref!"