About that, Coq uses something that proved itself to be rather usefull, 
though the problematic is a bit different. It's called notation scopes. 
The idea is that infix operators are defined in a specific scope. That 
you can either open locally using (here the scope is open)%scopeName, or 
globally by using Open Scope scopeName. When a scope is open, all the 
infix operators are interpreted as its definition in that scope. There 
are also a few more technicalities to make it even more fun (for 
instance, you can bind a scope to a type t, then, whenever an expression 
is inferred to be type t, the scope t is automatically opened, it's a 
very useful feature).

This allows a milde, but rather usable notation overloading.

I've been wondering for quite a while if such a policy would be 
reasonable/usefull for OCaml.


My two pennies,
Arnaud Spiwack

Richard Jones a écrit :
> If it is true that parts of the program will typically use a single
> class of operator, then what about a simple syntax extension like:
>
>   with BigInt
>     let a = b + c * d in
>
> Similar, in fact, to the very desirable "local open" feature
> (http://alain.frisch.fr/soft.html#openin)
>
> Rich.
>
>