diff options
author | 2015-01-12 14:24:01 +0100 | |
---|---|---|
committer | 2015-01-12 14:24:01 +0100 | |
commit | 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d (patch) | |
tree | c3703906dfa0b1d3c43380afa477dd62859da916 /kernel/typeops.mli | |
parent | e99e4006368fab3818812c6194d54465746c4566 (diff) |
Update test for #3363 now that Require is forbidden inside modules.
Diffstat (limited to 'kernel/typeops.mli')
0 files changed, 0 insertions, 0 deletions