diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 72f199efb5..2de77c29ad 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -589,7 +589,8 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp = let rec replace_idl = function | _,[] -> [] | id::idl,(id',obj)::tail when id = id' -> - if object_tag obj = "MODULE" then + let tag = object_tag obj in + if tag = "MODULE" or tag ="MODULE ALIAS" then (match idl with [] -> (id, in_module_alias (Some ({mod_entry_type = None; |