[Agda] dotted patterns

[Martín Hötzel Escardó]

I was working at the University and had this to compile in my computer 
there, with 2.6.0:

```
yoneda-lemma : {X : U} {x : X} {A : PrShf X} (η : Nat (Hom x) A)
              → yoneda-nat A (yoneda-elem A η) ≈ η
yoneda-lemma {X} {x} {A} η x (idp x) = idp (yoneda-elem A η)
```
But this was an accident with very old code, in which I decided to make 
some implicit argument explicit, and I forgot add the required dots.

At home, now, in another machine with Agda 2.6.0, it didn't compile. But 
I pulled the last version of Agda (2.6.0-3b39f0f) and it does compile 
with that.

Are non-linear patterns a new feature? Or a bug. If they are a feature, 
what is their specified behaviour?

Martin