The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  I'm trying to use Coq's List Notation of [ .. ; .. ; .. ].

  I try the following:

Require Import List.
Local Open Scope list_scope.

Eval compute in [1; 2].

  Instead of getting a (1 :: 2 :: nil), I get back

  Syntax error: [constr: lconstr] expected after 'in' ...

What am I doing wrong?