1
------------------------------------------------------------------------
2
-- Release notes for Agda 2 version 2.2.4
3
------------------------------------------------------------------------
5
Important changes since 2.2.2:
7
* Change to the semantics of "open import" and "open module". The
10
open import M <using/hiding/renaming>
15
open A <using/hiding/renaming>
19
import A <using/hiding/renaming>
22
The same translation is used for "open module M = E …". Declarations
23
involving the keywords as or public are changed in a corresponding
24
way ("as" always goes with import, and "public" always with open).
26
This change means that import directives do not affect the qualified
27
names when open import/module is used. To get the old behaviour you
28
can use the expanded version above.
30
* Names opened publicly in parameterised modules no longer inherit the
31
module parameters. Example:
36
module B (Y : Set) where
39
In Agda 2.2.2 B.X has type (Y : Set) → Set, whereas in Agda 2.2.4
42
* Previously it was not possible to export a given constructor name
43
through two different "open public" statements in the same module.
46
* Unicode subscript digits are now allowed for the hierarchy of
47
universes (Set₀, Set₁, …): Set₁ is equivalent to Set1.