From 9fbe91637e1b2521c5bdc4d561247b0ee9dfcee2 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 26 Jun 2009 22:56:35 +0000
Subject: 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
---
 library/declaremods.ml | 12 ++++--------
 1 file 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
-- 
cgit v1.2.3