20070530-5

When opening a module with implicit parameters locally the implicit parameters are instantiated.

Notes

  • The cause of the problem is that when opening a module under a context we have to create an auxiliary module abstracting over the context. In this process the implicit parameters are filled in by mistake.