Include Self (Type) Foo: applying a (Type) Functor to the current context

 If you have some Module Type F (X:Sig), and you are in a Module Type
 containing everything required to satisfy Sig (typically thanks to
 some earlier Include), then you can say Include Self Type F, and voila,
 objects of F are now added in your context, instantiated by local objects.
 Same behavior (hopefully) for modules and functors when using Include Self F.

 This experimental new command allows to easily produce static signatures
 out of functorial ones:

 Module Type F_static. Include Sig. Include Self F. End F_static.

 ... is similar to ...

 Module Type F_static. Declare Module X:Sig. Include F X. End F_static.

 ... but without the pollution of this artificial inner module X.

 This allow to split things in many othogonal components, and then mix them.
 It is a lightweight way to tackle the "diamond problem" of modular
 developpements without things like "overlapping" Include's (planned, but
 not yet there). See next commit for an example of use.

 Thanks to Elie for the debugging of my first ugly prototype...

 NB: According to Yann R.G., this is related with Scala's Traits.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12528 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions