The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Hi all,
I have the following trouble with notation on my Windows system.
I define the following notation:
=========================
Class N : Type.
Class epsilon (A a:N) : Prop.

Notation "A ε b" := (epsilon A b)  (at level 70).
...
=========================
and I obtain the following error:
Error: A notation must include at least one symbol.
The same program correctly runs on a Mac.
If someone has an idea?
Thanks in advance,
Richard

--

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard