Release notes for Agda version 2.4.2.5
======================================

Installation and infrastructure
-------------------------------

* Added support for GHC 7.10.3.

* Added `cpphs` Cabal flag

  Turn on/off this flag to choose cpphs/cpp as the C preprocessor.

  This flag is turn on by default.

  (This flag was added in Agda 2.4.2.1 but it was not documented)

Pragmas and options
-------------------

* Termination pragmas are no longer allowed inside `where` clauses
  [Issue [#1137](https://github.com/agda/agda/issues/1137)].

Type checking
-------------

* `with`-abstraction is more aggressive, abstracts also in types of
  variables that are used in the `with`-expressions, unless they are
  also used in the types of the
  `with`-expressions. [Issue [#1692](https://github.com/agda/agda/issues/1692)]

  Example:

  ```agda
  test : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
  test f b with a | f b
  test f b | .b | refl = f b
  ```

  Previously, `with` would not abstract in types of variables that
  appear in the `with`-expressions, in this case, both `f` and `b`,
  leaving their types unchanged.  Now, it tries to abstract in `f`, as
  only `b` appears in the types of the `with`-expressions which are
  `A` (of `a`) and `a ≡ b` (of `f b`).  As a result, the type of `f`
  changes to `(x : A) → b ≡ x` and the type of the goal to `b ≡ b` (as
  previously).

  This also affects `rewrite`, which is implemented in terms of
  `with`.

  ```agda
  test : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
  test f b rewrite f b = f b
  ```

  As the new `with` is not fully backwards-compatible, some parts of
  your Agda developments using `with` or `rewrite` might need
  maintenance.

Fixed issues
------------

See [bug tracker](https://github.com/agda/agda/issues)

[#1407](https://github.com/agda/agda/issues/1497)

[#1518](https://github.com/agda/agda/issues/1518)

[#1670](https://github.com/agda/agda/issues/1670)

[#1677](https://github.com/agda/agda/issues/1677)

[#1698](https://github.com/agda/agda/issues/1698)

[#1701](https://github.com/agda/agda/issues/1701)

[#1710](https://github.com/agda/agda/issues/1710)

[#1718](https://github.com/agda/agda/issues/1718)