2-2-4.txt

------------------------------------------------------------------------
-- 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

    open import M <using/hiding/renaming>

  now translates to

    import A
    open A <using/hiding/renaming>

  instead of

    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:

    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.