[Agda] [ANNOUNCE] Agda 2.5.4.2

[Sergei Meshveliani]

On Mon, 2018-10-29 at 23:17 +0000, Andres Sicard Ramirez wrote:
>  Dear all,
> 
> The Agda Team is very pleased to announce the release of Agda 2.5.4.2.
> 
> In this bug-fix release, we fixed a regression in Agda 2.5.4 related
> to slow type-checking with unsolved instance constraint (this fix
> wasn't included in the CHANGELOG by mistake, so see
> https://github.com/agda/agda/issues/3177 ) and we fixed a regression
> in Agda 2.5.4.1 related to the installation with some old versions of
> `cabal-install`. See the details and other changes in
> 
>     https://hackage.haskell.org/package/Agda-2.5.4.2/changelog
> 
> [..] 


1. What is, briefly, its relation to the Development version of  
   September 6, 2018 ?

2.
Also I have a certain application tested under  Agda-2.5.3 + lib-0.16,
and I try to port it to  Agda-2.5.4.2 + lib-0.17.
This occurs difficult.

For example, it imported _≟_ for Char by

  open import Data.Char as Char using (Char) renaming (_≟_ to _≟c_)

Now, I am somehow forced to write
  open import Data.Char as Char using (Char) 
  ...
  open StrictTotalOrder Char.strictTotalOrder using () 
                                      renaming (_≟_ to _≟c_)

Still this _≟c_ does not work as earlier. The code

  delimiters =  ' ' ∷ ',' ∷ ';' ...

  delimiter? :  Decidable (_∈ delimiters)
  delimiter? c =  any (c ≟c_) delimiters

is not type-checked any more. The report is

  ℕ != Char of type Set
  when checking that the expression any (c ≟c_) delimiters has type
  Relation.Nullary.Dec (c ∈ delimiters)

Has _≟_ changed its definition for Char ?

Thanks,

------
Sergei