mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 22:17:19 +03:00
7b5f4aa392
Fixes #111 Previously, if a module B imports a module A, then a module C imports B, the public names in A would also be visible to C (i.e. B would automatically reexport everything from A). This seems to be a bad default. This patch changes the default behaviour so that the only names exported from a module are those defined in that module. If B imports A and wants to reexport everything in A, then A should be imported with the "public" modifier (i.e. "import public A"). Several changes have been made to the prelude, since several prelude modules were taking advantage of the old broken behaviour. This may cause lots of things to break. Sorry. The fix is typically just to import the module you should have imported anyway :). |
||
---|---|---|
.. | ||
expected | ||
run | ||
test018.idr | ||
test018a.idr |