More monomorphic List.mem + List.assoc + ...

 To reduce the amount of syntactic noise, we now provide
 a few inner modules Int.List, Id.List, String.List, Sorts.List
 which contain some monomorphic (or semi-monomorphic) functions
 such as mem, assoc, ...

 NB: for Int.List.mem and co we reuse List.memq and so on.

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

15 files changed, 88 insertions, 80 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 01f90f6c6..bbac10f0f 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -278,8 +278,7 @@ let rec bind_primary_aliases map pat =
 	  List.fold_left bind_primary_aliases map1 lpat
 
 let bind_secondary_aliases map subst =
-  Id.Map.fold
-    (fun ids idp map -> (ids,List.assoc_f Id.equal idp map)::map) subst map
+  Id.Map.fold (fun ids idp map -> (ids,Id.List.assoc idp map)::map) subst map
 
 let bind_aliases patvars subst patt =
   let map = bind_primary_aliases [] patt in
@@ -349,7 +348,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let inject = function
       Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp)
     | Thesis (For rec_occ) ->
-	if not (List.mem rec_occ pat_vars) then
+	if not (Id.List.mem rec_occ pat_vars) then
 	  errorlabstrm "suppose it is"
 	    (str "Variable " ++ Nameops.pr_id rec_occ ++
 	       str " does not occur in pattern.");
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 673b749e1..30ed01c49 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1189,7 +1189,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	  execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
     | End_patt (id,(nparams,nhyps)),[] -> 
 	begin
-	  match List.assoc_f Id.equal id args with
+	  match Id.List.assoc id args with
 	      [None,br_args] -> 
 		let all_metas = 
 		  List.init (nparams + nhyps) (fun n -> mkMeta (succ n))  in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 947a1a482..c6bb9faa0 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -141,7 +141,8 @@ let sign_with_implicits r s nb_params =
     | [] -> []
     | sign::s ->
 	let sign' =
-	  if sign == Keep && List.mem i implicits then Kill Kother else sign
+	  if sign == Keep && Int.List.mem i implicits
+          then Kill Kother else sign
 	in sign' :: add_impl (succ i) s
   in
   add_impl (1+nb_params) s
@@ -657,7 +658,8 @@ and extract_cst_app env mle mlt kn args =
   (* Can we instantiate types variables for this constant ? *)
   (* In Ocaml, inside the definition of this constant, the answer is no. *)
   let instantiated =
-    if lang () == Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema)
+    if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints
+    then var2var' (snd schema)
     else instantiation schema
   in
   (* Then the expected type of this constant. *)
@@ -1048,7 +1050,7 @@ let extract_inductive env kn =
       | [] -> []
       | t::l ->
 	  let l' = filter (succ i) l in
-	  if isDummy (expand env t) || List.mem i implicits then l'
+	  if isDummy (expand env t) || Int.List.mem i implicits then l'
 	  else t::l'
     in filter (1+ind.ind_nparams) l
   in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 1e6a1fffc..22e7080e1 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1005,7 +1005,7 @@ let kill_some_lams bl (ids,c) =
 let kill_dummy_lams c =
   let ids,c = collect_lams c in
   let bl = List.map sign_of_id ids in
-  if not (List.mem Keep bl) then raise Impossible;
+  if not (List.memq Keep bl) then raise Impossible;
   let rec fst_kill n = function
     | [] -> raise Impossible
     | Kill _ :: bl -> n
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 083108bef..2556460f5 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -32,7 +32,7 @@ let unif t1 t2=
     match kind_of_term t with
 	Meta i->
 	  (try
-	     head_reduce (List.assoc_f Int.equal i !sigma)
+	     head_reduce (Int.List.assoc i !sigma)
 	   with Not_found->t)
       | _->t in
     Queue.add (t1,t2) bige;
@@ -105,7 +105,7 @@ let mk_rel_inst t=
     match kind_of_term t with
 	Meta n->
 	  (try
-	     mkRel (d+(List.assoc_f Int.equal n !rel_env))
+	     mkRel (d+(Int.List.assoc n !rel_env))
 	   with Not_found->
 	     let m= !new_rel in
 	       incr new_rel;
@@ -117,7 +117,7 @@ let mk_rel_inst t=
 
 let unif_atoms i dom t1 t2=
   try
-    let t=List.assoc_f Int.equal i (unif t1 t2) in
+    let t=Int.List.assoc i (unif t1 t2) in
       if isMeta t then Some (Phantom dom)
       else Some (Real(mk_rel_inst t,value i t1))
   with
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 95aaf4518..8edb16850 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -766,7 +766,7 @@ let build_proof
 			}
 		      in
 		      build_proof_args do_finalize new_infos  g
-		  | Const c when not (List.mem c fnames) ->
+		  | Const c when not (List.mem_f Constant.equal c fnames) ->
 		      let new_infos =
 			{ dyn_infos with
 			    info = (f,args)
@@ -915,7 +915,7 @@ let generalize_non_dep hyp g =
   let hyp_typ = pf_type_of g (mkVar hyp) in
   let to_revert,_ =
     Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
-      if List.mem hyp hyps
+      if Id.List.mem hyp hyps
         || List.exists (Termops.occur_var_in_decl env hyp) keep
 	|| Termops.occur_var env hyp hyp_typ
 	|| Termops.is_section_variable hyp (* should be dangerous *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index cb9d12c5e..e65ca94f0 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -367,7 +367,7 @@ let poseq_list_ids lcstr gl =
 let find_fapp (test:constr -> bool) g : fapp_info list =
   let pre_res = hdMatchSub (Tacmach.pf_concl g) test in
   let res =
-    List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in
+    List.fold_right (List.add_set Pervasives.(=)) pre_res [] in
   (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res);
   res)
 
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 91ea714c1..dd02dfe8d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -126,7 +126,7 @@ let rec replace_var_by_term_in_binder x_id term = function
   | [] -> []
   | (bt,t)::l ->
       (bt,replace_var_by_term x_id term t)::
-	if List.mem x_id (ids_of_binder bt)
+	if Id.List.mem x_id (ids_of_binder bt)
 	then l
 	else replace_var_by_term_in_binder x_id term l
 
@@ -134,14 +134,14 @@ let add_bt_names bt = List.append (ids_of_binder bt)
 
 let apply_args ctxt body args =
   let need_convert_id avoid id =
-    List.exists (is_free_in id) args || List.mem id avoid
+    List.exists (is_free_in id) args || Id.List.mem id avoid
   in
   let need_convert avoid  bt =
     List.exists (need_convert_id avoid) (ids_of_binder bt)
   in
   let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
     match na with
-       | Name id when List.mem id avoid ->
+       | Name id when Id.List.mem id avoid ->
 	   let new_id = Namegen.next_ident_away id avoid in
 	   Name new_id,Id.Map.add id new_id mapping,new_id::avoid
        | _ -> na,mapping,avoid
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index a16b5f0fe..79cba2c7c 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -199,7 +199,7 @@ let rec alpha_pat excluded pat =
 	let new_id = Indfun_common.fresh_id excluded "_x" in
 	PatVar(loc,Name new_id),(new_id::excluded),Id.Map.empty
     | PatVar(loc,Name id) ->
-	if List.mem id excluded
+	if Id.List.mem id excluded
 	then
 	  let new_id = Namegen.next_ident_away id excluded in
 	  PatVar(loc,Name new_id),(new_id::excluded),
@@ -208,7 +208,7 @@ let rec alpha_pat excluded pat =
     | PatCstr(loc,constr,patl,na) ->
 	let new_na,new_excluded,map =
 	  match na with
-	    | Name id when List.mem id excluded ->
+	    | Name id when Id.List.mem id excluded ->
 		let new_id = Namegen.next_ident_away id excluded in
 		Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty
 	    | _ -> na,excluded,Id.Map.empty
@@ -412,7 +412,7 @@ let is_free_in id =
     | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
     | GCast (_,b,CastCoerce) -> is_free_in b
   and is_free_in_br (_,ids,_,rt) =
-    (not (List.mem id ids)) && is_free_in rt
+    (not (Id.List.mem id ids)) && is_free_in rt
   in
   is_free_in
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 57019b3fa..a77968092 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -294,7 +294,9 @@ let check_not_nested forbidden e =
   let rec check_not_nested e =  
     match kind_of_term e with 
       | Rel _ -> ()
-      | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^Id.to_string x)
+      | Var x ->
+        if Id.List.mem x forbidden
+        then error ("check_not_nested : failure "^Id.to_string x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
       | Prod(_,t,b) -> check_not_nested t;check_not_nested b
@@ -652,7 +654,7 @@ let mkDestructEq :
   let to_revert =
     Util.List.map_filter
       (fun (id, _, t) ->
-        if List.mem id not_on_hyp || not (Termops.occur_term expr t)
+        if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t)
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
   let type_of_expr = pf_type_of g expr in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 5c057231a..4f96d7209 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -140,8 +140,7 @@ let rev_assoc k =
 let tag_hypothesis,tag_of_hyp, hyp_of_tag =
   let l = ref ([]:(Id.t * int) list) in
   (fun h id -> l := (h,id):: !l),
-  (fun h ->
-    try List.assoc_f Id.equal h !l with Not_found -> failwith "tag_hypothesis"),
+  (fun h -> try Id.List.assoc h !l with Not_found -> failwith "tag_hypothesis"),
   (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis")
 
 let hide_constr,find_constr,clear_tables,dump_tables =
@@ -1022,7 +1021,7 @@ let replay_history tactic_normalisation =
 	  begin
 	    try
 	      tclTHEN
-		(List.assoc_f Id.equal (hyp_of_tag e.id) tactic_normalisation)
+		(Id.List.assoc (hyp_of_tag e.id) tactic_normalisation)
 		(loop l)
 	    with Not_found -> loop l end
       | NEGATE_CONTRADICT (e2,e1,b) :: l ->
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index b74faf30b..4e9ca6ffc 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -546,30 +546,30 @@ let rec depend relie_on accu = function
   | act :: l ->
       begin match act with
 	| DIVIDE_AND_APPROX (e,_,_,_) ->
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            if Int.List.mem e.id relie_on then depend relie_on (act::accu) l
             else depend relie_on accu l
 	| EXACT_DIVIDE (e,_) ->
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            if Int.List.mem e.id relie_on then depend relie_on (act::accu) l
             else depend relie_on accu l
 	| WEAKEN (e,_) ->
-            if List.mem e relie_on then depend relie_on (act::accu) l
+            if Int.List.mem e relie_on then depend relie_on (act::accu) l
             else depend relie_on accu l
 	| SUM (e,(_,e1),(_,e2)) ->
-            if List.mem e relie_on then
+            if Int.List.mem e relie_on then
 	      depend (e1.id::e2.id::relie_on) (act::accu) l
             else
 	      depend relie_on accu l
 	| STATE {st_new_eq=e;st_orig=o} ->
-            if List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l
+            if Int.List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l
             else depend relie_on accu l
 	| HYP e ->
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            if Int.List.mem e.id relie_on then depend relie_on (act::accu) l
             else depend relie_on accu l
 	| FORGET_C _ -> depend relie_on accu l
 	| FORGET _ -> depend relie_on accu l
 	| FORGET_I _ -> depend relie_on accu l
 	| MERGE_EQ (e,e1,e2) ->
-            if List.mem e relie_on then
+            if Int.List.mem e relie_on then
 	      depend (e1.id::e2::relie_on) (act::accu) l
             else
 	      depend relie_on accu l
@@ -673,7 +673,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
            try let _ = loop2 sys in raise NO_CONTRADICTION
            with UNSOLVABLE ->
              let relie_on,path = depend [] [] (history ()) in
-             let dc,_ = List.partition (fun (_,id,_) -> List.mem id relie_on) decomp in
+             let dc,_ = List.partition (fun (_,id,_) -> Int.List.mem id relie_on) decomp in
              let red = List.map (fun (x,_,_) -> x) dc in
              (red,relie_on,decomp,path))
         sys_exploded
@@ -705,7 +705,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
         let s2' = List.map remove_int s2 in
         let (r1,relie1) = solve s1'
 	and (r2,relie2) = solve s2' in
-	let (eq,id1,id2) = Util.List.assoc_f Int.equal id explode_map in
+	let (eq,id1,id2) = Int.List.assoc id explode_map in
 	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))],
         eq.id :: Util.List.union Int.equal relie1 relie2
       with FULL_SOLUTION (x0,x1) -> (x0,x1)
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index af833dacb..5416e936c 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -23,7 +23,7 @@ let string_of_global r =
     | [] -> ""
     | m::_ ->
       let s = Names.Id.to_string m in
-      if List.mem s meaningful_submodule then s^"." else ""
+      if Util.String.List.mem s meaningful_submodule then s^"." else ""
   in
   prefix^(Names.Id.to_string (Nametab.basename_of_global r))
 
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 26fab4ac2..bf46065d0 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -13,6 +13,8 @@
 (************************************************************************)
 
 open Pp
+open Util
+open Names
 
 (* Utility Functions *)
 
@@ -37,7 +39,7 @@ let get_module_path_of_full_path path =
 (*CSC: not exist two modules whose dir_paths are one a prefix of the other *)
 let remove_module_dirpath_from_dirpath ~basedir dir =
   if Libnames.is_dirpath_prefix_of basedir dir then
-   let ids = Names.DirPath.repr dir in
+   let ids = DirPath.repr dir in
    let rec remove_firsts n l =
     match n,l with
        (0,l) -> l
@@ -47,11 +49,11 @@ let remove_module_dirpath_from_dirpath ~basedir dir =
     let ids' =
      List.rev
       (remove_firsts
-        (List.length (Names.DirPath.repr basedir))
+        (List.length (DirPath.repr basedir))
         (List.rev ids))
     in
      ids'
-  else Names.DirPath.repr dir
+  else DirPath.repr dir
 ;;
 
 
@@ -60,21 +62,22 @@ let get_uri_of_var v pvars =
    function
       [] -> Errors.error ("Variable "^v^" not found")
     | he::tl as modules ->
-       let dirpath = Names.DirPath.make modules in
-        if List.mem (Names.Id.of_string v) (Decls.last_section_hyps dirpath) then
+       let dirpath = DirPath.make modules in
+       if Id.List.mem (Id.of_string v) (Decls.last_section_hyps dirpath)
+       then
          modules
-        else
+       else
          search_in_open_sections tl
   in
    let path =
-    if List.mem v pvars then
+    if String.List.mem v pvars then
       []
     else
-      search_in_open_sections (Names.DirPath.repr (Lib.cwd ()))
+      search_in_open_sections (DirPath.repr (Lib.cwd ()))
    in
     "cic:" ^
      List.fold_left
-      (fun i x -> "/" ^ Names.Id.to_string x ^ i) "" path
+      (fun i x -> "/" ^ Id.to_string x ^ i) "" path
 ;;
 
 type tag =
@@ -105,31 +108,31 @@ let ext_of_tag =
 exception FunctorsXMLExportationNotImplementedYet;;
 
 let subtract l1 l2 =
- let l1' = List.rev (Names.DirPath.repr l1) in
- let l2' = List.rev (Names.DirPath.repr l2) in
+ let l1' = List.rev (DirPath.repr l1) in
+ let l2' = List.rev (DirPath.repr l2) in
   let rec aux =
    function
       he::tl when tl = l2' -> [he]
     | he::tl -> he::(aux tl)
     | [] -> assert (l2' = []) ; []
   in
-   Names.DirPath.make (List.rev (aux l1'))
+   DirPath.make (List.rev (aux l1'))
 ;;
 
 let token_list_of_path dir id tag =
   let token_list_of_dirpath dirpath =
-   List.rev_map Names.Id.to_string (Names.DirPath.repr dirpath) in
-  token_list_of_dirpath dir @ [Names.Id.to_string id ^ "." ^ (ext_of_tag tag)]
+   List.rev_map Id.to_string (DirPath.repr dirpath) in
+  token_list_of_dirpath dir @ [Id.to_string id ^ "." ^ (ext_of_tag tag)]
 
 let token_list_of_kernel_name tag =
  let id,dir = match tag with
    | Variable kn ->
-       Names.Label.to_id (Names.label kn), Lib.cwd ()
+       Label.to_id (Names.label kn), Lib.cwd ()
    | Constant con ->
-       Names.Label.to_id (Names.con_label con),
+       Label.to_id (Names.con_label con),
        Lib.remove_section_part (Globnames.ConstRef con)
    | Inductive kn ->
-       Names.Label.to_id (Names.mind_label kn),
+       Label.to_id (Names.mind_label kn),
        Lib.remove_section_part (Globnames.IndRef (kn,0))
  in
  token_list_of_path dir id (etag_of_tag tag)
@@ -188,7 +191,7 @@ let typeur sigma metamap =
   let rec type_of env cstr=
     match Term.kind_of_term cstr with
     | T.Meta n ->
-          (try T.strip_outer_cast (Util.List.assoc_f Int.equal n metamap)
+          (try T.strip_outer_cast (Int.List.assoc n metamap)
            with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term"))
     | T.Rel n ->
         let (_,_,ty) = Environ.lookup_rel n env in
@@ -198,7 +201,7 @@ let typeur sigma metamap =
           let (_,_,ty) = Environ.lookup_named id env in
           ty
         with Not_found ->
-          Errors.anomaly ~label:"type_of" (str "variable " ++ Names.Id.print id ++ str " unbound"))
+          Errors.anomaly ~label:"type_of" (str "variable " ++ Id.print id ++ str " unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
         Typeops.type_of_constant_type env (cb.Declarations.const_type)
@@ -447,8 +450,8 @@ print_endline "PASSATO" ; flush stdout ;
                 let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in
                 let he1'' =
                  String.concat "/"
-                  (List.rev_map Names.Id.to_string he1') ^ "/"
-                 ^ (Names.Id.to_string he1_id) ^ ".var"
+                  (List.rev_map Id.to_string he1') ^ "/"
+                 ^ (Id.to_string he1_id) ^ ".var"
                 in
                  (he1'',he2)::subst, extra_args, uninst
            in
@@ -493,13 +496,13 @@ print_endline "PASSATO" ; flush stdout ;
                Acic.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
            | Term.Var id ->
 	      let pvars = Termops.ids_of_named_context (Environ.named_context env) in
-	      let pvars = List.map Names.Id.to_string pvars in
-              let path = get_uri_of_var (Names.Id.to_string id) pvars in
+	      let pvars = List.map Id.to_string pvars in
+              let path = get_uri_of_var (Id.to_string id) pvars in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                if is_a_Prop innersort  && expected_available then
                 add_inner_type fresh_id'' ;
                Acic.AVar
-                (fresh_id'', path ^ "/" ^ (Names.Id.to_string id) ^ ".var")
+                (fresh_id'', path ^ "/" ^ (Id.to_string id) ^ ".var")
            | Term.Evar (n,l) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
@@ -602,7 +605,7 @@ print_endline "PASSATO" ; flush stdout ;
            | Term.LetIn (n,s,t,d) ->
               let id =
                match n with
-                   Names.Anonymous -> Names.Id.of_string "_X"
+                   Names.Anonymous -> Id.of_string "_X"
                  | Names.Name id -> id
               in
               let n' =
@@ -877,7 +880,7 @@ let acic_object_of_cic_object sigma obj =
                          in
                          let dummy_never_used =
                           let s = "dummy_never_used" in
-                           Acic.ARel (s,99,s,Names.Id.of_string s)
+                           Acic.ARel (s,99,s,Id.of_string s)
                          in
                           final_env,final_idrefs,
                            (hid,(n,Acic.Def (at,dummy_never_used)))::atl
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index abd6b3b73..83a4d425b 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -21,6 +21,8 @@ let verbose = ref false;;
 let print_if_verbose s = if !verbose then print_string s;;
 
 open Decl_kinds
+open Names
+open Util
 
 (* filter_params pvars hyps *)
 (* filters out from pvars (which is a list of lists) all the variables *)
@@ -35,18 +37,19 @@ let filter_params pvars hyps =
       let ids' = id::ids in
       let ids'' =
        "cic:/" ^
-        String.concat "/" (List.rev_map Names.Id.to_string ids') in
+        String.concat "/" (List.rev_map Id.to_string ids') in
       let he' =
-       ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in
+       ids'', List.rev (List.filter (function x -> String.List.mem x hyps) he)
+      in
       let tl' = aux ids' tl in
        match he' with
           _,[] -> tl'
         | _,_  -> he'::tl'
  in
   let cwd = Lib.cwd () in
-  let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
+  let cwdsp = Libnames.make_path cwd (Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
-   aux (Names.DirPath.repr modulepath) (List.rev pvars)
+   aux (DirPath.repr modulepath) (List.rev pvars)
 ;;
 
 (* The computation is very inefficient, but we can't do anything *)
@@ -54,15 +57,15 @@ let filter_params pvars hyps =
 (* module.                                                       *)
 let search_variables () =
   let cwd = Lib.cwd () in
-  let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
+  let cwdsp = Libnames.make_path cwd (Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
    let rec aux =
     function
        [] -> []
      | he::tl as modules ->
         let one_section_variables =
-         let dirpath = Names.DirPath.make (modules @ Names.DirPath.repr modulepath) in
-          let t = List.map Names.Id.to_string (Decls.last_section_hyps dirpath) in
+         let dirpath = DirPath.make (modules @ DirPath.repr modulepath) in
+          let t = List.map Id.to_string (Decls.last_section_hyps dirpath) in
            [he,t]
         in
          one_section_variables @ aux tl
@@ -110,7 +113,7 @@ let theory_filename xml_library_root =
   match xml_library_root with
     None -> None  (* stdout *)
   | Some xml_library_root' ->
-     let toks = List.map Names.Id.to_string (Names.DirPath.repr (Lib.library_dp ())) in
+     let toks = List.map Id.to_string (DirPath.repr (Lib.library_dp ())) in
      (* theory from A/B/C/F.v goes into A/B/C/F.theory *)
      let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")
@@ -150,7 +153,7 @@ let print_object uri obj sigma filename =
 
 let string_list_of_named_context_list =
  List.map
-  (function (n,_,_) -> Names.Id.to_string n)
+  (function (n,_,_) -> Id.to_string n)
 ;;
 
 (* Function to collect the variables that occur in a term. *)
@@ -159,7 +162,7 @@ let string_list_of_named_context_list =
 let find_hyps t =
   let rec aux l t =
    match Term.kind_of_term t with
-      Term.Var id when not (List.mem id l) ->
+      Term.Var id when not (Id.List.mem id l) ->
        let (_,bo,ty) = Global.lookup_named id in
         let boids =
          match bo with
@@ -193,7 +196,7 @@ let find_hyps t =
   and map_and_filter l =
    function
       [] -> []
-    | (n,_,_)::tl when not (List.mem n l) -> n::(map_and_filter l tl)
+    | (n,_,_)::tl when not (Id.List.mem n l) -> n::(map_and_filter l tl)
     | _::tl -> map_and_filter l tl
   in
    aux [] t
@@ -208,11 +211,11 @@ let mk_variable_obj id body typ =
    | Some bo -> find_hyps bo, Some (Unshare.unshare bo)
  in
   let hyps' = find_hyps typ @ hyps in
-  let hyps'' = List.map Names.Id.to_string hyps' in
+  let hyps'' = List.map Id.to_string hyps' in
   let variables = search_variables () in
   let params = filter_params variables hyps'' in
    Acic.Variable
-    (Names.Id.to_string id, unsharedbody, Unshare.unshare typ, params)
+    (Id.to_string id, unsharedbody, Unshare.unshare typ, params)
 ;;
 
 
@@ -222,10 +225,10 @@ let mk_constant_obj id bo ty variables hyps =
  let params = filter_params variables hyps in
   match bo with
      None ->
-      Acic.Constant (Names.Id.to_string id,None,ty,params)
+      Acic.Constant (Id.to_string id,None,ty,params)
    | Some c ->
       Acic.Constant
-       (Names.Id.to_string id, Some (Unshare.unshare c), ty,params)
+       (Id.to_string id, Some (Unshare.unshare c), ty,params)
 ;;
 
 let mk_inductive_obj sp mib packs variables nparams hyps finite =
@@ -371,7 +374,7 @@ let print internal glob_ref kind xml_library_root =
        let (_,body,typ) = Global.lookup_named id in
         Cic2acic.Variable kn,mk_variable_obj id body typ
     | Globnames.ConstRef kn ->
-       let id = Names.Label.to_id (Names.con_label kn) in
+       let id = Label.to_id (Names.con_label kn) in
        let cb = Global.lookup_constant kn in
        let val0 = Declareops.body_of_constant cb in
        let typ = cb.Declarations.const_type in
@@ -444,7 +447,7 @@ let _ =
          (* I saved in the Pfedit.set_xml_cook_proof callback.          *)
         let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in
          show_pftreestate internal fn pftreestate
-	  (Names.Label.to_id (Names.con_label kn)) ;
+	  (Label.to_id (Names.con_label kn)) ;
          proof_to_export := None)
 ;;
 
@@ -508,7 +511,7 @@ let _ = Hook.set Lexer.xml_output_comment (theory_output_string ~do_not_quote:tr
 
 let uri_of_dirpath dir =
   "/" ^ String.concat "/"
-    (List.rev_map Names.Id.to_string (Names.DirPath.repr dir))
+    (List.rev_map Id.to_string (DirPath.repr dir))
 ;;
 
 let _ =
@@ -527,5 +530,5 @@ let _ =
   Hook.set Library.xml_require
     (fun d -> theory_output_string
       (Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>"
-       (uri_of_dirpath d) (Names.DirPath.to_string d)))
+       (uri_of_dirpath d) (DirPath.to_string d)))
 ;;