[Agda] ANNOUNCE: Agda 2.4.2.1

[Sergei Meshveliani]

On Fri, 2014-11-14 at 19:21 -0500, Andrés Sicard-Ramírez wrote:
> Hi,
> 
> Agda 2.4.2.1 has been released.
> 
> [..]


This is on the language change.
For example, I have 

-------------------------------------------------------------------------
module Membership2 {α α= : Level} (A : Setoid α α=)
  where
  ...

  x∈del-x→anyRepeats : (_≟_ : Decidable₂ _≈_) → ∀ {x xs} → 
                                        x ∈ del _≟_ x xs → AnyRepeats xs

  x∈del-x→anyRepeats _   {_} {[]}     ()
  x∈del-x→anyRepeats _≟_ {x} {y ∷ xs} x∈del-x-y:xs  with x ≟ y
  ...
      | yes x=y =  hereRep y∈xs   where  x∈xs : x ∈ xs
                                         x∈xs = x∈del-x-y:xs

                                         y∈xs = cong₁∈ x=y x∈xs
  ... | no x≉y =  thereRep anyRep-xs
                  where
                  x∈y:del-xs :  x ∈ y ∷ (del _≟_ x xs)
                  x∈y:del-xs =  x∈del-x-y:xs

                  x∈del-xs : x ∈ del _≟_ x xs
                  x∈del-xs with  x∈y:del-xs
                  ...           | here x=y       = ⊥-elim $ x≉y x=y
                  ...           | there x∈del-xs = x∈del-xs

                  anyRep-xs : AnyRepeats xs
                  anyRep-xs = x∈del-x→anyRepeats _≟_ x∈del-xs
--------------------------------------------------------------------------

This means a lemma:  
     "if  x  is in  (delete x xs),  then  xs  has a repetition in it".

It is accepted in  Agda 2.4.2  and is forbidden in  Agda 2.4.2.1 : 

"Cannot `with` on variable x∈del-x-y:xs bound in a module telescope
(or patterns of a parent clause)
when inferring the type of x∈del-x-y:xs
".

I wonder: how to fix the code? 
Does not this above code look natural?

(I fear, that there are many similar places in my application).

Thanks,

------
Sergei