On 5/13/07, ls-ocaml-developer-2006@m-e-leypold.de
<ls-ocaml-developer-2006@m-e-leypold.de> wrote:
>
> 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

This is what the simple openin extension does (emulates using camlp4).

http://alain.frisch.fr/soft#openin

-- 
Nicolas Pouillard