Release notes for Agda 2 version 2.2.4
======================================

Important changes since 2.2.2:

* Change to the semantics of `open import` and `open module`. The
  declaration

  ```agda
  open import M <using/hiding/renaming>
  ```

  now translates to

  ```agda
  import A
  open A <using/hiding/renaming>
  ```

  instead of

  ```agda
  import A <using/hiding/renaming>
  open A
  ```

  The same translation is used for `open module M = E …`. Declarations
  involving the keywords as or public are changed in a corresponding
  way (`as` always goes with import, and `public` always with open).

  This change means that import directives do not affect the qualified
  names when open import/module is used. To get the old behaviour you
  can use the expanded version above.

* Names opened publicly in parameterised modules no longer inherit the
  module parameters. Example:

  ```agda
  module A where
    postulate X : Set

  module B (Y : Set) where
    open A public
  ```

  In Agda 2.2.2 `B.X` has type `(Y : Set) → Set`, whereas in
  Agda 2.2.4 `B.X` has type Set.

* Previously it was not possible to export a given constructor name
  through two different `open public` statements in the same module.
  This is now possible.

* Unicode subscript digits are now allowed for the hierarchy of
  universes (`Set₀`, `Set₁`, …): `Set₁` is equivalent to `Set1`.