Less restrictive --without-K [Re: [Agda] no longer type checks]

[Andreas Abel]

On 30.05.13 6:56 PM, Nils Anders Danielsson wrote:
> On 2013-05-30 18:12, Andrés Sicard-Ramírez wrote:
>> Before your patch this proof was accepted using the --without-K
>> option:
>
> My --without-K library also fails to type check now:
>
>    http://www.cse.chalmers.se/~nad/repos/equality/

Thanks for the pointer and sorry for breaking this.  I could not get to 
the point of error yet, need to run it on a bigger machine...

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/