Arnaud Spiwack <aspiwack@lix.polytechnique.fr> writes:

> 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.

I'd like to have a way to open moduls in a restricted scop, like

  with module Foo 
     
      let x = f a b c in

          ...
  end


which would be equivalent to 

      let x = Foo.f a b c in

          ...

if f is in Foo.

Regards -- Markus