diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-21 11:42:50 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-21 11:42:50 +0000 |
| commit | 3857df7438d49220fc1bfc85883ad33868c35ee7 (patch) | |
| tree | 4a75737d4245934b345a628f806d1c6a96f1d75d /library/declaremods.ml | |
| parent | 05f91178923218b864d8c921dfb557c7c13f14ca (diff) | |
Correction bug #1969.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11483 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.ml')
| -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 72f199efb..2de77c29a 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; |