diff options
| -rw-r--r-- | library/declaremods.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 52fa945692..f1a2c9e6c7 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1059,19 +1059,15 @@ let rec update_include (sub,mbids,msid,objs) = | (id,obj)::tail -> if object_tag obj = "INCLUDE" then let ((me,is_mod),substobjs,substituted) = out_include obj in - if not (is_mod) then - let substobjs' = update_include substobjs in - (id, in_include ((me,true),substobjs',substituted)):: - (replace_include tail) - else - (id,obj)::(replace_include tail) + let substobjs' = update_include substobjs in + (id, in_include ((me,true),substobjs',substituted)):: + (replace_include tail) else (id,obj)::(replace_include tail) in (sub,mbids,msid,replace_include objs) - - + let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = let fs = Summary.freeze_summaries () in |