[Agda] dotted pattern for pair

[Sergei Meshveliani]

Hi,

For _=p_ being a coordinatewise equality on  ℕ × ℕ,  the function

  pr :  pairToNZ Preserves _=p_ ⟶ _='p_
  pr {(n , e)} {.(n , e)} (PE.refl , PE.refl) =  ...

is type-checked in Agda-2.5.1.1 and is not type-checked in Development
Agda of September 16, 2016.
The latter version does not accept this dotted pattern and insists on
the pattern  {(.n , e.)}  instead.

I point out the difference, for any occasion.

Regards,

------
Sergei