[Agda] A different implementation of --without-K

[Nils Anders Danielsson]

On 2013-11-28 23:34, Andreas Abel wrote:
> Yes, some of the fail test cases seem only to be there to document
> what *is* rejected.  I do not know what purpose this serves, since I
> would expect only stuff there that *must be* rejected.

The point is that the semantics of --without-K should not be changed by
accident. These examples "must" be rejected until we make a conscious
decision to change the semantics.

-- 
/NAD