idris-lang/Idris-dev — pull request #945 by david-christiansen (2014-03-02 23:14:45+00:00)
Title: New syntax for documentation comments

Implementation entailed removing documentation from the idris_implicits
field of IState, which is why so many files are touched. See mailing list post (reproduced in a comment here) for details.