[Agda] "Hiding of record parameters"

[Andrés Sicard-Ramírez]

On 3 March 2016 at 10:51, Sergei Meshveliani <mechvel at botik.ru> wrote:
> You wrote yesterday (on the bug tracker) about fixing the bug of
>
>   Hiding of record parameters leads to hiding mismatch in
>   checkInternal (#1759).
>
> Probably this implies a certain change/restriction in the record usage.
> Because  Development Agda of March 3 2016  does not accept some of my
> code related to the record usage.
>
> Can you, please, formulate:
> what is the change in the record declaration and usage?

See https://github.com/agda/agda/blob/master/CHANGELOG#L989-L1003


-- 
Andrés