Using namespaces

[braibant]

Should the implementation of the signature descriptions make it possible to describe nested namespaces?

[gasche]

I think we don't need it for a toy presentation (the best we can aim for in an article setting anyway). The point of signature descriptions is to expose the public interface of the module, but it need not absolutely mirror the ML signature source.