[Agda] Renaming of a module, associated with a record, doesn't hide the original name.

[effectfully]

Hi.

    module _ where

    open import Data.Nat

    module M where
      record R : Set where
        z = 0
    open M renaming (module R to R')

   test = {!!}

In `test' both `R.z' and `R'.z'are in scope.

If I write

    open M renaming (module R to R'; R to R')

instead, then `R.z' is not in scope in `test'.

If I write

    open M renaming (R to R')

then both `R.z' and `R'.z' are in scope again.

I guess in the first and the third cases there should be in scope only
`R'.z' and `R.z' accordingly. Is the current behaviour a bug or am I
misunderstanding something?