edwinb/Idris-dev — pull request #128 by startling (2012-12-14 00:05:53+00:00)
Title: Allow documentation comments for records.

Before, you'd get this kind of parse error with this kind of file:

````idris
-- | Some comment.
record Id : Type -> Type where
mkId : (runId : a) -> Id a
````

````
% idris todo.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 0.9.5.2
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help

"./todo.idr" (line 2, column 1):
unexpected "r"
expecting "public", "abstract", "private" or "class"
````