From b0272a5a98d0f8dd56a56bceda6f80eb6ee70a61 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Mon, 4 Feb 2008 11:49:46 +0000
Subject: declaremods.ml Patch function load_include

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10503 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declaremods.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 8cfd7e1ae6..44907fd589 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -964,11 +964,7 @@ let load_include  i (oname,((me,is_mod),substobjs,substituted)) =
   let prefix = (dir,(mp1,empty_dirpath)) in
     match substituted with
 	Some seg -> 
-	  if is_mod then
-	    load_objects i prefix seg
-	  else 
-	    if i = 1 then
-	      load_objects i prefix seg
+	  load_objects i prefix seg
       | None ->  ()
 
 let open_include i (oname,((me,is_mod),substobjs,substituted)) =
-- 
cgit v1.2.3