The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  I'm trying to use Notation together with Scopes.

  The following is a minimal example which fails


Inductive foo := fA | fB.
Variable fAdd : foo -> foo -> foo.

Notation "A + B" := (fAdd A B) : foo_scope.

Check (fA + fB) % foo_scope.

>>> Error: Unknown scope delimiting key foo_scope.

How should I fix this? I'm rather baffled -- % foo_scope should mean that the "+" uses the Notation defined above, to be fAdd. Furthermore, the Notation line should have defined scope foo_scope and added a notation to it.

What am I doing wrong?

Thanks!