Problem with some notation

[fblanqui]

Hi. PG gets frozen with the following file when we reach the line 3:

Axiom Ninterval: nat -> nat -> Prop.
Notation "[ n  '....'  m ]" := (Ninterval n m).
Notation "x 'BETWEEN' n 'AND' m " := ([n .... m] x) (at level 1).
Axiom something_else : Prop.