On 2015-10-08 11:05, Nils Anders Danielsson wrote: > Thanks, this looks like a bug: > > https://github.com/agda/agda/issues/1681 The bug has now been fixed. -- /NAD