optim: Idset au lieu de list

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2160 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 6 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 9ca23646f2..33f93a8acc 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -50,11 +50,11 @@ let extract_module m =
 type extracted_env = {
   mutable visited : Refset.t;
   mutable to_extract : global_reference list;
-  mutable modules : identifier list
+  mutable modules : Idset.t
 }
 
 let empty () = 
-  { visited = ml_extractions (); to_extract = []; modules = []}
+  { visited = ml_extractions (); to_extract = []; modules = Idset.empty }
 
 let rec visit_reference m eenv r =
   let r' = match r with
@@ -68,8 +68,8 @@ let rec visit_reference m eenv r =
     eenv.visited <- Refset.add r' eenv.visited;
     if m then begin 
       let m_name = module_of_r r' in 
-      if not (List.mem m_name eenv.modules) then begin
-	eenv.modules <- m_name :: eenv.modules;
+      if not (Idset.mem m_name eenv.modules) then begin
+	eenv.modules <- Idset.add m_name eenv.modules;
  	List.iter (visit_reference m eenv) (extract_module m_name)
       end
     end;
@@ -129,7 +129,7 @@ let extract_env rl =
 
 let modules_extract_env m =
   let eenv = empty () in
-  eenv.modules <- [m];
+  eenv.modules <- Idset.singleton m;
   List.iter (visit_reference true eenv) (extract_module m);
   eenv.modules, List.rev eenv.to_extract
 
@@ -257,7 +257,7 @@ let _ =
 			      to_appear= []} in
 	      let decls = optimize dummy_prm (decl_of_refs refs) in
 	      let decls = add_ml_decls dummy_prm decls in
-	      List.iter 
+	      Idset.iter 
 		(fun m ->
 		   let f = (String.uncapitalize (string_of_id m))
 			   ^ (file_suffix lang) in