@@ -1136,7 +1136,8 @@ accData a n ns = do addAcc n a
1136 mapM_ (`addAcc` a) ns
1136 mapM_ (`addAcc` a) ns
1138pRecord :: SyntaxInfo -> IParser PDecl
1138pRecord :: SyntaxInfo -> IParser PDecl
1139+pRecord syn = do doc <- option "" (pDocComment '|')
1139−pRecord syn = do acc <- pAccessibility
1140+ acc <- pAccessibility
1140 reserved "record"
1141 reserved "record"
1141 fc <- pfc
1142 fc <- pfc
1142 tyn_in <- pfName
1143 tyn_in <- pfName
@@ -1154,7 +1155,7 @@ pRecord syn = do acc <- pAccessibility
1154 syn_namespace syn }
1155 syn_namespace syn }
1155 let fns = getRecNames rsyn cty
1156 let fns = getRecNames rsyn cty
1156 mapM_ (\n -> addAcc n acc) fns
1157 mapM_ (\n -> addAcc n acc) fns
1157− return $ PRecord "" rsyn fc tyn ty cdoc cn cty
1158+ return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1159 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkSet n)]
1160 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkSet n)]
1160 ++ getRecNames syn sc
1161 ++ getRecNames syn sc