agda/agda — pull request #6 by jespercockx (2014-06-25 05:16:54+00:00)
Title: Agda now reduces types before checking that they are data types

This was a super silly mistake I made in my hack for solving Issue 1023 (https://code.google.com/p/agda/issues/detail?id=1023), which caused the termination checker to complain a LOT more than necessary when --without-K was enabled (see also https://code.google.com/p/agda/issues/detail?id=1214). If possible, please check that there are no other mistakes (it's only a few lines).