[Agda] darcs - dev-version fail

[Ulf Norell]

On Thu, Nov 21, 2013 at 5:51 PM, Sergei Meshveliani <mechvel at botik.ru>wrote:

> Dear Agda developers,
> I have the following problems.
>
> > agda -V
>
> prints    Agda version 2.3.3
>
> But it cannot type-check anything:
>
>   module DPrelude
>   where
>   open import Level using (Level; suc; _⊔_)
>

The syntax has changed slightly from version 2.3.2. You need to indent the
"where" or put it on the same line as "module".

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131121/f17fde72/attachment.html