[Agda] Strange bug

[Guillaume Allais]

Hi Phil,

This particularly annoying bug has been fixed in 2.5.4.2:
https://github.com/agda/agda/issues/3199

Cheers,
--
gallais

On 25/02/2019 00:31, Philip Wadler wrote:
> I am getting a strange bug.
> 
> An internal error has occurred. Please report this as a bug.
>> Location of the error:
>> src/full/Agda/TypeChecking/Serialise/Instances/Common.hs:178
> 
> 
> Relevant source files attached. The error occurs in CoercionsS.lagda.
> 
> What is the best way to report this, please?   -- P
> 
> 
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
> 
> 
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190225/2ae898f6/attachment.sig>