diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-26 22:56:35 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-26 22:56:35 +0000 |
| commit | 9fbe91637e1b2521c5bdc4d561247b0ee9dfcee2 (patch) | |
| tree | 024584566dc3b7bc5e4fbf410d8519735ab6e7da /library/declaremods.ml | |
| parent | ed5d9cb136384ce0f7363a1c839ff0f9a7e9df7b (diff) | |
propagation sur le trunk du commit 12101
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12212 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.ml')
| -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 52fa94569..f1a2c9e6c 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 |