Release notes for Agda version 2.5.1.1
======================================

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

* Added support for GHC 8.0.1.

* Documentation is now built with Python >=3.3, as done by
  [readthedocs.org](https://readthedocs.org/).

Bug fixes
---------

* Fixed a serious performance problem with instance search

  Issues [#1952](https://github.com/agda/agda/issues/1952) and
  [#1998](https://github.com/agda/agda/issues/1998). Also related:
  [#1955](https://github.com/agda/agda/issues/1955) and
  [#2025](https://github.com/agda/agda/issues/2025)

* Interactively splitting variable with `C-c C-c` no longer introduces
  new trailing patterns.  This fixes
  Issue [#1950](https://github.com/agda/agda/issues/1950).

  ```agda
  data Ty : Set where
    _⇒_ : Ty → Ty → Ty

  ⟦_⟧ : Ty → Set
  ⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧

  data Term : Ty → Set where
    K : (A B : Ty) → Term (A ⇒ (B ⇒ A))

  test : (A : Ty) (a : Term A) → ⟦ A ⟧
  test A a = {!a!}
  ```

  Before change, case splitting on `a` would give

  ```agda
  test .(A ⇒ (B ⇒ A)) (K A B) x x₁ = ?
  ```

  Now, it yields

  ```agda
  test .(A ⇒ (B ⇒ A)) (K A B) = ?
  ```

* In literate TeX files, `\begin{code}` and `\end{code}` can be
  preceded (resp. followed) by TeX code on the same line. This fixes
  Issue [#2077](https://github.com/agda/agda/issues/2077).

* Other issues fixed (see
  [bug tracker](https://github.com/agda/agda/issues)):

  [#1951](https://github.com/agda/agda/issues/1951) (mixfix binders
  not working in 'syntax')

  [#1967](https://github.com/agda/agda/issues/1967) (too eager
  insteance search error)

  [#1974](https://github.com/agda/agda/issues/1974) (lost constraint
  dependencies)

  [#1982](https://github.com/agda/agda/issues/1982) (internal error in
  unifier)

  [#2034](https://github.com/agda/agda/issues/2034) (function type
  instance goals)

Compiler backends
-----------------

* UHC compiler backend

  Added support for UHC 1.1.9.4.