diff options
Diffstat (limited to 'tools/depend.ml')
| -rw-r--r-- | tools/depend.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/depend.ml b/tools/depend.ml index 57c9fd0172..573f399f14 100644 --- a/tools/depend.ml +++ b/tools/depend.ml @@ -180,6 +180,7 @@ and add_modtype bv mty = (function (_, Pwith_type td) -> add_type_declaration bv td | (_, Pwith_module lid) -> addmodule bv lid) cstrl + | Pmty_typeof m -> add_module bv m and add_signature bv = function [] -> () |