From e93d18133d7f6d11bb8676ccbed982db8c7c24d6 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 28 Oct 2009 13:15:41 +0000
Subject: Same as commit 12430 but with the good version of the function
 iter_all_segment

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

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 53f9617c50..68ce86b3ae 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -923,12 +923,10 @@ let iter_all_segments f =
   let _ =
     MPmap.iter
       (fun _ (prefix,objects) ->
-	 let apply_obj (id,obj) = match object_tag obj with 
+	 let rec apply_obj (id,obj) = match object_tag obj with 
 	   | "INCLUDE" -> 
-	       let (_,(_,mp,objs)) =  out_include obj in 
-	       let apply_include (id,obj) =
-		 f (make_oname prefix id) obj in
-		 List.iter apply_include objs
+	       let (_,(_,_,objs)) =  out_include obj in 
+		 List.iter apply_obj objs
 		   
 	   | _ -> f (make_oname prefix id) obj in
 	   List.iter apply_obj objects)
-- 
cgit v1.2.3