[Agda] emacs agda mode bug (with expansion, coinduction)

[Florent Balestrieri]

Hello,

I came across a bug in the agda2 emacs mode.
Please use the attached file to reproduce the behaviour (I am using Agda 
2.2.7)

if you expand the line:

... | u | eq = ?

by case-splitting `eq', it gets replaced by:

.Sandbox.WeirdWith.with-7 ♯eq .(tt ∷ xs') (_∷_ .tt {xs'} xs≈) = ?

instead of:

... | .(tt ∷ xs') | _∷_ .tt {xs'} xs≈ = ?


All the best,
-- Florent

-------------- next part --------------
module Sandbox.WeirdWith where

open import Coinduction
open import Data.Stream
open import Data.Unit

tts : Stream ⊤
tts = tt ∷ ♯ tts

f : (u : Stream ⊤) → u ≈ tts → ⊤

f .(tt ∷ ♯u) (_∷_ tt {♯u} ♯eq)
  with ♭ ♯u | ♭ ♯eq

... | u | eq = {!!}

-- .Sandbox.WeirdWith.with-7 ♯eq .(tt ∷ xs') (_∷_ .tt {xs'} xs≈) = ?
-- ... | .(tt ∷ xs') | _∷_ .tt {xs'} xs≈ = {!!}