The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Hi all,
suppose I want to overload some notation, let us say in this context:

Inductive U1 := A.
Inductive U2 := B.

I want to define the notations

Notation "'ε'" := (A).
Notation "'ε'" := (B).

in such a way that both (ε : U1) and (ε : U2) type-checks in the same
context (in particular with the same opened scopes).
How can I do this (without using that hideous '%<scope>')?

I just want a way to make ': U1' open the U1_scope and ': U2' open the
U2_scope. I tried 'Bind Scope' but with no success. I have read the
manual, but it is not very clear on that part.

------------------------------
Bind Scope u with U1.
Bind Scope v with U2.

Notation "'ε'" := (A) : u.
Notation "'ε'" := (B) : v.

Open Scope u.
Open Scope v.

Delimit Scope u with u_.
Delimit Scope v with v_.

Bind Scope u_ with U1.
Bind Scope v_ with U2.

Check (ε : U1).