aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/smartlocate.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-16 13:46:22 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-16 13:46:22 +0000
commit68dfbbc355bdcab7f7880bacc4be6fe337afa800 (patch)
tree54dbae884dfed975adaaf5f5c5f1767ebe3bfe4b /interp/smartlocate.ml
parent56c24c0c704119430ee5fde235cc8c76dc2746c3 (diff)
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
Diffstat (limited to 'interp/smartlocate.ml')
0 files changed, 0 insertions, 0 deletions