[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[Jesper Cockx]

I expect the problem is because of the fix of
https://github.com/agda/agda/issues/4189. In the Changelog, it says:
-
>
> Record constructors can no longer be qualified by the record module. (See
> issue #4189 <https://github.com/agda/agda/issues/4189>.)
>
> record Foo : Set where
>   constructor foo
>
> works = foo
> fails = Foo.foo
>
> -- Jesper


On Sun, Dec 29, 2019 at 10:55 PM <mechvel at scico.botik.ru> wrote:

> On 2019-12-22 14:41, Andres Sicard Ramirez wrote:
> > Dear all,
> >
> > The Agda Team is very pleased to announce the first release candidate
> > of Agda 2.6.1. We plan to release 2.6.1 in three weeks.
> > [..]
>
>
> Please, see the attached letter. This is a candidate for a bug report.
>
> If you do not guess what is the source of the effect, then I could check
> the
> difference more precisely.
>
> --
> SM
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191230/a8cfd390/attachment.html>