diff options
| author | Maxime Dénès | 2015-01-17 11:48:21 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:16:44 +0530 |
| commit | d187edf437ca4dac73b1da5d434cdf164c129319 (patch) | |
| tree | e659a1e577e9281aa6507fea520fd94c9c57009b /dev | |
| parent | 18ac6441e93ca670740a1b874033ec016d4f1392 (diff) | |
Partially revert "Forbid Require inside interactive modules and module types."
This reverts commit 6d5b56d971506dfadcfc824bfbb09dc21718e42b but does not put
back in place the Requires inside modules that were found in the std lib.
Conflicts:
kernel/safe_typing.ml
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions