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

[Nicolas Pouillard]

On 08/10/2015 10:09 AM, Andreas Abel wrote:
> Maybe it is worth continuing the discussion on the Agda list, if we talk
> about changes to the Agda language.
>
> Here is a proposal:
>
> * Remove qualification by data/record type name.

I find this feature useful, for instance to qualify certain 
data-constructors for instance:

```
   suc-inj : ∀{x y} → ℕ.suc x ≡ suc y → x ≡ y
```

> * default to applying renaming/using/hiding also to the module
> * if renaming/using/hiding is given for a module name explicitly, it
> overrides the default behavior

I'm in favor of this change though. Some old code which explicitly 
mention both namespaces should still be accepted:

```
open M using (module X; X) hiding (module Y; Y)
```

This way the only non-backward compatible situation requires to hide the 
module:

Before:

```
open M using (X)
```

After:

```
open M using (X) hiding (module X)
```

Best regards,
-- NP