------------------------------------------------------------------------
-- Release notes for Agda 2 version 2.4.2
------------------------------------------------------------------------

Important changes since 2.4.0:

Installation and Infrastructure
===============================

Pragmas and Options
===================

* The option --compile-no-main was renamed to --compile --no-main.

* The option --termination-depth is now obsolete.

  The default termination depth is now infinity instead of
  (previously) 1.  This means that setting --termination-depth might
  now make the termination checker *weaker* (instead of stronger).
  However, there is no guaranteed effect of setting
  --termination-depth any more.  The flag is only kept for debugging
  Agda.

  For example, the following code now passes the termination checker
  (needed higher --termination-depth before):

    f : Nat → Nat
    g : Nat → Nat

    f zero                = zero
    f (suc zero)          = zero
    f (suc (suc zero))    = zero
    f (suc (suc (suc n))) = g n     -- decrease by 3

    g n = f (suc (suc n))           -- increase by 2

  [See also issue 709.]

Language
========

Goal and error display
======================

Type checking
=============

Compiler backends
=================

Tools
=====

Emacs mode
----------

LaTeX-backend
-------------