[Agda] Bugs

[Nils Anders Danielsson]

On 2009-02-18 14:54, Pierre Hyvernat wrote:
> (1) the first one is easily replicable and only concerns the emacs
> interface. The string "--" inside a comment seems to have strange
> effects in Emacs

This bug has already been reported. I just pushed a fix.

> (2) the second is probably more important: I managed to get the
> following message:
> 
>   An internal error has occurred. Please report this as a bug.
>   Location of the error: src/full/Agda/TypeChecking/Substitute.hs:130

This bug has also been reported before (twice), see
http://code.google.com/p/agda/issues/detail?id=120.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.