Moving Utils.list_* to a proper CList module, which includes stdlib

List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.

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

29 files changed, 118 insertions, 118 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 53c146bfc..423c95509 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -367,7 +367,7 @@ let discriminate_tac cstr p gls =
 let build_term_to_complete uf meta pac =
   let cinfo = get_constructor_info uf pac.cnode in
   let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
-  let dummy_args = List.rev (list_tabulate meta pac.arity) in
+  let dummy_args = List.rev (List.tabulate meta pac.arity) in
   let all_args = List.rev_append real_args dummy_args in
     applistc (mkConstruct cinfo.ci_constr) all_args
 
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 5e128bc42..f2f978ccd 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -57,7 +57,7 @@ let intern_hyp iconstr globs = function
       Hprop (intern_statement iconstr globs st)
 
 let intern_hyps iconstr globs hyps =
-  snd (list_fold_map (intern_hyp iconstr) globs hyps)
+  snd (List.fold_map (intern_hyp iconstr) globs hyps)
 
 let intern_cut intern_it globs cut=
   let nglobs,nstat=intern_it globs cut.cut_stat in
@@ -74,10 +74,10 @@ let intern_hyp_list args globs =
   let intern_one globs (loc,(id,opttyp)) =
     (add_var id globs),
     (loc,(id,Option.map (intern_constr globs) opttyp)) in
-  list_fold_map intern_one globs args
+  List.fold_map intern_one globs args
 
 let intern_suffices_clause globs (hyps,c) =
-  let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in
+  let nglobs,nhyps = List.fold_map (intern_hyp intern_constr) globs hyps in
     nglobs,(nhyps,intern_constr_or_thesis nglobs c)
 
 let intern_fundecl args body globs=
@@ -340,7 +340,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	(fun (loc,(id,_)) ->
 	   GVar (loc,id)) params in
     let dum_args=
-      list_tabulate
+      List.tabulate
 	(fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false)))
 	oib.Declarations.mind_nrealargs in
       glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 31e15081b..1a0d05047 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -857,7 +857,7 @@ let build_per_info etype casee gls =
     match etype with
 	ET_Induction -> mind.mind_nparams_rec,Some (snd ind)
       | _ -> mind.mind_nparams,None in
-  let params,real_args = list_chop nparams args in
+  let params,real_args = List.chop nparams args in
   let abstract_obj c body =
     let typ=pf_type_of gls c in
       lambda_create env (typ,subst_term c body) in
@@ -953,7 +953,7 @@ let rec tree_of_pats ((id,_) as cpl) pats =
 		    let nexti i ati =
 		      if i = pred cnum then
 			let nargs =
-			  list_map_i (fun j a -> (a,ati.(j))) 0 args in
+			  List.map_i (fun j a -> (a,ati.(j))) 0 args in
 			  Some (Idset.singleton id,
 				tree_of_pats cpl (nargs::rest_args::stack))
 		      else None
@@ -998,7 +998,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 			  let nexti i ati =
 			    if i = pred cnum then
 			      let nargs =
-				list_map_i (fun j a -> (a,ati.(j))) 0 args in
+				List.map_i (fun j a -> (a,ati.(j))) 0 args in
 				Some (Idset.add id ids,
 				      add_branch cpl (nargs::rest_args::stack)
 					(skip_args t ids (Array.length ati)))
@@ -1013,7 +1013,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 			  let mapi i ati bri =
 			    if i = pred cnum then
 			      let nargs =
-				list_map_i (fun j a -> (a,ati.(j))) 0 args in
+				List.map_i (fun j a -> (a,ati.(j))) 0 args in
 				append_branch cpl 0
 				  (nargs::rest_args::stack) bri
 			    else bri in
@@ -1051,7 +1051,7 @@ let thesis_for obj typ per_info env=
     errorlabstrm "thesis_for"
       ((Printer.pr_constr_env env obj) ++ spc () ++
 	 str"cannot give an induction hypothesis (wrong inductive type).") in
-  let params,args = list_chop per_info.per_nparams all_args in
+  let params,args = List.chop per_info.per_nparams all_args in
   let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
     errorlabstrm "thesis_for"
       ((Printer.pr_constr_env env obj) ++ spc () ++
@@ -1182,7 +1182,7 @@ let hrec_for fix_id per_info gls obj_id =
   let rc,hd1=decompose_prod typ in
   let cind,all_args=decompose_app typ in
   let ind = destInd cind in assert (ind=per_info.per_ind);
-  let params,args= list_chop per_info.per_nparams all_args in
+  let params,args= List.chop per_info.per_nparams all_args in
   assert begin
     try List.for_all2 eq_constr params per_info.per_params with
         Invalid_argument _ -> false end;
@@ -1203,8 +1203,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	  match List.assoc id args with
 	      [None,br_args] -> 
 		let all_metas = 
-		  list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps)  in
-		let param_metas,hyp_metas = list_chop nparams all_metas in
+		  List.tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps)  in
+		let param_metas,hyp_metas = List.chop nparams all_metas in
 		  tclTHEN
 		    (tclDO nhrec introf)
 		    (tacnext 
@@ -1221,7 +1221,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let ctyp=pf_type_of gls casee in
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
 	let _ = assert (destInd hd = ind) in (* just in case *)
-	let params,real_args = list_chop nparams all_args in
+	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
 	  let typ=pf_type_of gls c in
 	    lambda_create env (typ,subst_term c body) in
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index b6b7e5833..8cceb2a11 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -349,7 +349,7 @@ let rec mp_renaming_fun mp = match mp with
   | MPfile _ ->
       assert (modular ()); (* see [at_toplevel] above *)
       assert (get_phase () = Pre);
-      let current_mpfile = (list_last (get_visible ())).mp in
+      let current_mpfile = (List.last (get_visible ())).mp in
       if mp <> current_mpfile then mpfiles_add mp;
       [string_of_modfile mp]
 
@@ -496,7 +496,7 @@ let fstlev_ks k = function
 let pp_ocaml_local k prefix mp rls olab =
   (* what is the largest prefix of [mp] that belongs to [visible]? *)
   assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
-  let rls' = list_skipn (mp_length prefix) rls in
+  let rls' = List.skipn (mp_length prefix) rls in
   let k's = fstlev_ks k rls' in
   (* Reference r / module path mp is of the form [<prefix>.s.<...>]. *)
   if not (visible_clash prefix k's) then dottify rls'
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 588fe0cf2..b5cdec3ec 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -150,9 +150,9 @@ let factor_fix env l cb msb =
   if n = 1 then [|l|], recd, msb
   else begin
     if List.length msb < n-1 then raise Impossible;
-    let msb', msb'' = list_chop (n-1) msb in
+    let msb', msb'' = List.chop (n-1) msb in
     let labels = Array.make n l in
-    list_iter_i
+    List.iter_i
       (fun j ->
 	 function
 	   | (l,SFBconst cb') ->
@@ -207,7 +207,7 @@ let env_for_mtb_with_def env mp seb idl =
   in
   let l = label_of_id (List.hd idl) in
   let spot = function (l',SFBconst _) -> l = l' | _ -> false in
-  let before = fst (list_split_when spot sig_b) in
+  let before = fst (List.split_when spot sig_b) in
   Modops.add_signature mp before empty_delta_resolver env
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0556f6d77..e1bbcf9c7 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -193,7 +193,7 @@ let parse_ind_args si args relmax =
 
 let oib_equal o1 o2 =
   id_ord o1.mind_typename o2.mind_typename = 0 &&
-  list_equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
+  List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
   begin match o1.mind_arity, o2.mind_arity with
   | Monomorphic {mind_user_arity=c1; mind_sort=s1},
     Monomorphic {mind_user_arity=c2; mind_sort=s2} ->
@@ -206,10 +206,10 @@ let mib_equal m1 m2 =
   m1.mind_record = m2.mind_record &&
   m1.mind_finite = m2.mind_finite &&
   m1.mind_ntypes = m2.mind_ntypes &&
-  list_equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
+  List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
   m1.mind_nparams = m2.mind_nparams &&
   m1.mind_nparams_rec = m2.mind_nparams_rec &&
-  list_equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
+  List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
   m1.mind_constraints = m2.mind_constraints
 
 (*S Extraction of a type. *)
@@ -439,7 +439,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | _ -> []
 	in
 	let field_names =
-	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
+	  List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
 	assert (List.length field_names = List.length typ);
 	let projs = ref Cset.empty in
 	let mp,d,_ = repr_mind kn in
@@ -674,7 +674,7 @@ and extract_cst_app env mle mlt kn args =
   let mla =
     if not magic1 then
       try
-	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
+	let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
 	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
       with _ -> mla
@@ -697,7 +697,7 @@ and extract_cst_app env mle mlt kn args =
     (* Partially applied function with some logical arg missing.
        We complete via eta and expunge logical args. *)
     let ls' = ls-la in
-    let s' = list_skipn la s in
+    let s' = List.skipn la s in
     let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
     let e = anonym_or_dummy_lams (mlapp head mla) s' in
     put_magic_if magic2 (remove_n_lams (List.length optdummy) e)
@@ -729,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let la = List.length args in
   assert (la <= ls + params_nb);
   let la' = max 0 (la - params_nb) in
-  let args' = list_lastn la' args in
+  let args' = List.lastn la' args in
   (* Now, we build the expected type of the constructor *)
   let metas = List.map new_meta args' in
   (* If stored and expected types differ, then magic! *)
@@ -758,7 +758,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
     then put_magic_if (magic2 && not magic1) (head mla)
     else (* [ params_nb <= la <= ls + params_nb ] *)
       let ls' = params_nb + ls - la in
-      let s' = list_lastn ls' s in
+      let s' = List.lastn ls' s in
       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
       put_magic_if magic2 (anonym_or_dummy_lams (head mla) s')
 
@@ -847,7 +847,7 @@ let decomp_lams_eta_n n m env c t =
   let rels',c = decompose_lam c in
   let d = n - m in
   (* we'd better keep rels' as long as possible. *)
-  let rels = (list_firstn d rels) @ rels' in
+  let rels = (List.firstn d rels) @ rels' in
   let eta_args = List.rev_map mkRel (interval 1 d) in
   rels, applist (lift d c,eta_args)
 
@@ -886,7 +886,7 @@ let extract_std_constant env kn body typ =
     and m = nb_lam body in
     if n <= m then decompose_lam_n n body
     else
-      let s,s' = list_chop m s in
+      let s,s' = List.chop m s in
       if List.for_all ((=) Keep) s' &&
 	(lang () = Haskell || sign_kind s <> UnsafeLogicalSig)
       then decompose_lam_n m body
@@ -895,7 +895,7 @@ let extract_std_constant env kn body typ =
   (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
   let rels, c =
     let n = List.length rels in
-    let s,s' = list_chop n s in
+    let s,s' = List.chop n s in
     let k = sign_kind s in
     let empty_s = (k = EmptySig || k = SafeLogicalSig) in
     if lang () = Ocaml && empty_s && not (gentypvar_ok c)
@@ -904,8 +904,8 @@ let extract_std_constant env kn body typ =
     else rels,c
   in
   let n = List.length rels in
-  let s = list_firstn n s in
-  let l,l' = list_chop n l in
+  let s = List.firstn n s in
+  let l,l' = List.chop n l in
   let t' = type_recomp (l',t') in
   (* The initial ML environment. *)
   let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 3b89386d4..3716695b8 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -534,7 +534,7 @@ let is_regular_match br =
 	match pat with
 	  | Pusual r -> r
 	  | Pcons (r,l) ->
-	    if not (list_for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
+	    if not (List.for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
 	    then raise Impossible;
 	    r
 	  | _ -> raise Impossible
@@ -636,9 +636,9 @@ let eta_red e =
 	  if m = n then
 	    [], f, a
 	  else if m < n then
-	    list_skipn m ids, f, a
+	    List.skipn m ids, f, a
 	  else (* m > n *)
-	    let a1,a2 = list_chop (m-n) a in
+	    let a1,a2 = List.chop (m-n) a in
 	    [], MLapp (f,a1), a2
 	in
 	let p = List.length args in
@@ -969,7 +969,7 @@ and simpl_case o typ br e =
 	    else ([], Pwild, ast_pop f)
 	  in
 	  let brl = Array.to_list br in
-	  let brl_opt = list_filter_i (fun i _ -> not (Intset.mem i ints)) brl in
+	  let brl_opt = List.filter_i (fun i _ -> not (Intset.mem i ints)) brl in
 	  let brl_opt = brl_opt @ [last_br] in
 	  MLcase (typ, e, Array.of_list brl_opt)
 	| None -> MLcase (typ, e, br)
@@ -1022,8 +1022,8 @@ let kill_dummy_lams c =
     | Keep :: bl -> fst_kill (n+1) bl
   in
   let skip = max 0 ((fst_kill 0 bl) - 1) in
-  let ids_skip, ids = list_chop skip ids in
-  let _, bl = list_chop skip bl in
+  let ids_skip, ids = List.chop skip ids in
+  let _, bl = List.chop skip bl in
   let c = named_lams ids_skip c in
   let ids',c = kill_some_lams bl (ids,c) in
   ids, named_lams ids' c
@@ -1051,7 +1051,7 @@ let case_expunge s e =
   let m = List.length s in
   let n = nb_lams e in
   let p = if m <= n then collect_n_lams m e
-  else eta_expansion_sign (list_skipn n s) (collect_lams e) in
+  else eta_expansion_sign (List.skipn n s) (collect_lams e) in
   kill_some_lams (List.rev s) p
 
 (*s [term_expunge] takes a function [fun idn ... id1 -> c]
@@ -1085,7 +1085,7 @@ let kill_dummy_args ids r t =
 	let a = List.map (killrec n) a in
 	let a = List.map (ast_lift k) a in
 	let a = select_via_bl bl (a @ (eta_args k)) in
-	named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
+	named_lams (List.firstn k ids) (MLapp (ast_lift k e, a))
     | e when found n e ->
 	let a = select_via_bl bl (eta_args m) in
 	named_lams ids (MLapp (ast_lift m e, a))
@@ -1164,7 +1164,7 @@ let general_optimize_fix f ids n args m c =
     | MLrel j when v.(j-1)>=0 ->
 	if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
     | _ -> raise Impossible
-  in list_iter_i aux args;
+  in List.iter_i aux args;
   let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
   let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in
   let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 1211bbf17..8659de03e 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -30,7 +30,7 @@ let se_iter do_decl do_spec =
     | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
     | MTwith (mt,ML_With_type(idl,l,t))->
 	let mp_mt = msid_of_mt mt in
-	let l',idl' = list_sep_last idl in
+	let l',idl' = List.sep_last idl in
 	let mp_w =
 	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
 	in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 34ae1f9ad..951049b7b 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -114,7 +114,7 @@ let pp_one_field r i = function
 
 let pp_field r fields i = pp_one_field r i (List.nth fields i)
 
-let pp_fields r fields = list_map_i (pp_one_field r) 0 fields
+let pp_fields r fields = List.map_i (pp_one_field r) 0 fields
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
@@ -189,7 +189,7 @@ let rec pp_expr par env args =
 	hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
     | MLglob r ->
 	(try
-	   let args = list_skipn (projection_arity r) args in
+	   let args = List.skipn (projection_arity r) args in
 	   let record = List.hd args in
 	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
 	 with _ -> apply (pp_global Term r))
@@ -642,7 +642,7 @@ and pp_module_type params = function
   | MTwith(mt,ML_With_type(idl,vl,typ)) ->
       let ids = pp_parameters (rename_tvars keywords vl) in
       let mp_mt = msid_of_mt mt in
-      let l,idl' = list_sep_last idl in
+      let l,idl' = List.sep_last idl in
       let mp_w =
 	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
       in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2dd07b2f2..6151abf6e 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -671,7 +671,7 @@ let add_implicits r l =
 	else err (int i ++ str " is not a valid argument number for " ++
 		  safe_pr_global r)
     | ArgId id ->
-	(try list_index (Name id) names
+	(try List.index (Name id) names
 	 with Not_found ->
 	   err (str "No argument " ++ pr_id id ++ str " for " ++
 		safe_pr_global r))
@@ -877,7 +877,7 @@ let extract_inductive r s l optstr =
 	Lib.add_anonymous_leaf (in_customs (g,[],s));
 	Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))
 	  optstr;
-	list_iter_i
+	List.iter_i
 	  (fun j s ->
 	     let g = ConstructRef (ip,succ j) in
 	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 7abb4dc52..f4cc397bc 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -142,7 +142,7 @@ let build_atoms gl metagen side cciterm =
 	  let g i _ (_,_,t) =
 	    build_rec env polarity (lift i t) in
 	  let f l =
-	    list_fold_left_i g (1-(List.length l)) () l in
+	    List.fold_left_i g (1-(List.length l)) () l in
 	    if polarity && (* we have a constant constructor *)
 	      array_exists (function []->true|_->false) v
 	    then trivial:=true;
@@ -152,7 +152,7 @@ let build_atoms gl metagen side cciterm =
 	  let v =(ind_hyps 1 i l gl).(0) in
 	  let g i _ (_,_,t) =
 	    build_rec (var::env) polarity (lift i t) in
-	    list_fold_left_i g (2-(List.length l)) () v
+	    List.fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
 	  let var=mkMeta (metagen true) in
 	    build_rec (var::env) polarity b
@@ -224,7 +224,7 @@ let build_formula side nam typ gl metagen=
 		  | And(_,_,_)        -> Rand
 		  | Or(_,_,_)         -> Ror
 		  | Exists (i,l) ->
-		      let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in
+		      let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in
 			Rexists(m,d,trivial)
 		  | Forall (_,a) -> Rforall
 		  | Arrow (a,b) -> Rarrow in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index e3367b4c2..414afad46 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -112,7 +112,7 @@ let mk_open_instance id gl m t=
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
-  let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in
+  let revt=substl (List.tabulate (fun i->mkRel (m-i)) m) t in
   let rec aux n avoid=
     if n=0 then [] else
       let nid=(fresh_id avoid var_id gl) in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 37d9edef8..7acabaaa4 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -129,7 +129,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
        let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
 	 it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
-       let newhyps=list_tabulate myterm lp in
+       let newhyps=List.tabulate myterm lp in
 	 tclIFTHENELSE
 	   (tclTHENLIST
 	      [generalize newhyps;
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 6d00e8d9f..c648939bb 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -191,9 +191,9 @@ let empty_seq depth=
    depth=depth}
 
 let expand_constructor_hints =
-  list_map_append (function
+  List.map_append (function
     | IndRef ind ->
-	list_tabulate (fun i -> ConstructRef (ind,i+1))
+	List.tabulate (fun i -> ConstructRef (ind,i+1))
 	  (Inductiveops.nconstructors ind)
     | gr ->
 	[gr])
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 33ea0ac8a..c3726f1a8 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -124,7 +124,7 @@ let unif_atoms i dom t1 t2=
     | Not_found ->Some (Phantom dom)
 
 let renum_metas_from k n t= (* requires n = max (free_rels t) *)
-  let l=list_tabulate (fun i->mkMeta (k+i)) n in
+  let l=List.tabulate (fun i->mkMeta (k+i)) n in
     substl l t
 
 let more_general (m1,t1) (m2,t2)=
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8ea4be631..0796930fc 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -93,7 +93,7 @@ let observe_tac s = observe_tac_stream (str s)
 
 let list_chop ?(msg="") n l =
   try
-    list_chop n l
+    List.chop n l
   with Failure (msg') ->
     failwith (msg ^ msg')
 
@@ -319,7 +319,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	      )
     in
     let new_type_of_hyp,ctxt_size,witness_fun =
-      list_fold_left_i
+      List.fold_left_i
 	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
 	   try
 	     let witness = Intmap.find i sub in
@@ -1168,7 +1168,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		typess
 	    in
 	    let pte_to_fix,rev_info =
-	      list_fold_left_i
+	      List.fold_left_i
 		(fun i (acc_map,acc_info) (pte,_,_) ->
 		   let infos = info_array.(i) in
 		   let type_args,_ = decompose_prod infos.types in
@@ -1557,7 +1557,7 @@ let prove_principle_for_gen
 (* 	     str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
 (* 	     str "npost_rec_arg := " ++ int npost_rec_arg ); *)
   let (post_rec_arg,pre_rec_arg) =
-    Util.list_chop npost_rec_arg princ_info.args
+    Util.List.chop npost_rec_arg princ_info.args
   in
   let rec_arg_id =
     match List.rev post_rec_arg with
@@ -1624,7 +1624,7 @@ let prove_principle_for_gen
 	  Elim.h_decompose_and (mkVar hid);
 	  (fun g ->
 	     let new_hyps = pf_ids_of_hyps g in
-	     tcc_list := List.rev (list_subtract new_hyps (hid::hyps));
+	     tcc_list := List.rev (List.subtract new_hyps (hid::hyps));
 	     if !tcc_list = []
 	     then
 	       begin
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e2dc149b0..f2eb4b23c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -88,7 +88,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     Nameops.out_name x,None,compose_prod real_args (mkSort new_sort)
   in
   let new_predicates =
-    list_map_i
+    List.map_i
       change_predicate_sort
       0
       princ_type_info.predicates
@@ -252,7 +252,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
   let pre_res =
     replace_vars
-      (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
+      (List.map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
       (lift (List.length ptes_vars) pre_res)
   in
   it_mkProd_or_LetIn
@@ -460,7 +460,7 @@ let get_funs_constant mp dp =
       let first_params = List.hd l_params  in
       List.iter
 	(fun params ->
-	   if not (list_equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params)
+	   if not (List.equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params)
 	   then error "Not a mutal recursive block"
 	)
 	l_params
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index d11c01672..1c2193449 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -89,7 +89,7 @@ let combine_results
   in (* and then we flatten the map *)
   {
     result = List.concat pre_result;
-    to_avoid = list_union res1.to_avoid res2.to_avoid
+    to_avoid = List.union res1.to_avoid res2.to_avoid
   }
 
 
@@ -269,7 +269,7 @@ let make_discr_match_el  =
   end
 *)
 let make_discr_match_brl i =
-  list_map_i
+  List.map_i
     (fun j (_,idl,patl,_) ->
        if j=i
        then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref))
@@ -659,7 +659,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let case_pats = build_constructors_of_type ind [] in
 	assert (Array.length case_pats = 2);
 	let brl =
-	  list_map_i
+	  List.map_i
 	    (fun i x -> (Loc.ghost,[],[case_pats.(i)],x))
 	    0
 	    [lhs;rhs]
@@ -748,7 +748,7 @@ and build_entry_lc_from_case env funname make_discr
 	{
 	  result = List.concat (List.map (fun r -> r.result) results);
 	  to_avoid =
-	    List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
+	    List.fold_left (fun acc r -> List.union acc r.to_avoid) [] results
 	}
 
 and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
@@ -818,7 +818,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
       	let those_pattern_preconds =
 	  (List.flatten
 	    (
-	      list_map3
+	      List.map3
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
 		 let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in
@@ -977,7 +977,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let mib,_ = Global.lookup_inductive ind in
 		    let nparam = mib.Declarations.mind_nparams in
 		    let params,arg' =
-		      ((Util.list_chop nparam args'))
+		      ((Util.List.chop nparam args'))
 		    in
 		    let rt_typ =
 		       GApp(Loc.ghost,
@@ -1000,7 +1000,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      match kind_of_term eq'_as_constr with
 			| App(_,[|_;_;ty;_|]) ->
 			    let ty = Array.to_list (snd (destApp ty)) in
-			    let ty' = snd (Util.list_chop nparam ty) in
+			    let ty' = snd (Util.List.chop nparam ty) in
 			    List.fold_left2
 			      (fun acc var_as_constr arg ->
 				 if isRel var_as_constr
@@ -1238,7 +1238,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
   let l = ref [] in
   let _ =
     try
-      list_iter_i
+      List.iter_i
 	(fun i ((n,nt,is_defined) as param) ->
 	   if array_for_all
 	     (fun l ->
@@ -1362,7 +1362,7 @@ let do_build_inductive
   in
   let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
     let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list  =
-      (snd (list_chop nrel_params funargs))
+      (snd (List.chop nrel_params funargs))
     in
     List.fold_right
       (fun (n,t,is_defined) acc ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 52562fb37..18b2bbe2f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -21,7 +21,7 @@ let is_rec_info scheme_info =
       Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
     )
   in
-  Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
+  Util.List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
 
 let choose_dest_or_ind scheme_info =
     if is_rec_info scheme_info
@@ -337,7 +337,7 @@ let generate_principle  on_error
 	in
 	let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
 	let _ =
-	  list_map_i
+	  List.map_i
 	    (fun i x ->
 	       let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
 	       let princ_type = Typeops.type_of_constant (Global.env()) princ
@@ -392,7 +392,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	if List.length names = 1 then 1
 	else error "Recursive argument must be specified"
       | Some wf_arg ->
-	  list_index (Name wf_arg) names
+	  List.index (Name wf_arg) names
   in
   let unbounded_eq =
     let f_app_args =
@@ -516,7 +516,7 @@ let decompose_lambda_n_assum_constr_expr =
 	    (n - nal_length) 
 	    (Constrexpr.CLambdaN(lambda_loc,bl,e'))
   	else
-	  let nal_keep,nal_expr = list_chop n nal in 
+	  let nal_keep,nal_expr = List.chop n nal in 
 	  (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
 	   Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
 	  )
@@ -548,7 +548,7 @@ let decompose_prod_n_assum_constr_expr =
 	    (if bl = [] then e' else (Constrexpr.CLambdaN(lambda_loc,bl,e')))
   	else
 	  (* let _ = Pp.msgnl (str "second case") in  *)
-	  let nal_keep,nal_expr = list_chop n nal in 
+	  let nal_keep,nal_expr = List.chop n nal in 
 	  (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
 	   Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
 	  )
@@ -585,7 +585,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	    let lnal' = List.length nal' in 
 	    if lnal' >= lnal 
 	    then 
-	      let old_nal',new_nal' = list_chop lnal nal' in 
+	      let old_nal',new_nal' = List.chop lnal nal' in 
 	      rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(make_assoc assoc old_nal' nal)) bl' 
 		(if new_nal' = [] && rest = []
 		 then  typ' 
@@ -593,7 +593,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 		 then CProdN(Loc.ghost,rest,typ')
 		 else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ'))
 	    else 
-	      let captured_nal,non_captured_nal = list_chop lnal' nal in 
+	      let captured_nal,non_captured_nal = List.chop lnal' nal in 
 	      rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (make_assoc assoc nal' captured_nal))
 		bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ'))
 	  | _ -> assert false
@@ -789,7 +789,7 @@ let rec chop_n_arrow n t =
 		    else
 		      let new_t' =
 			Constrexpr.CProdN(Loc.ghost,
-					((snd (list_chop n nal)),k,t'')::nal_ta',t')
+					((snd (List.chop n nal)),k,t'')::nal_ta',t')
 		      in
 		      raise (Stop new_t')
 		in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2f6a6a7d7..1d1089a54 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -370,7 +370,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       in
       (* in fact we must also add the parameters to the constructor args *)
       let constructor_args g =
-	let params_id = fst (list_chop princ_infos.nparams args_names) in
+	let params_id = fst (List.chop princ_infos.nparams args_names) in
 	(List.map mkVar params_id)@((constructor_args g))
       in
       (* We then get the constructor corresponding to this branch and
@@ -446,7 +446,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	)
 	lemmas_types_infos
     in
-    let param_names = fst (list_chop princ_infos.nparams args_names) in
+    let param_names = fst (List.chop princ_infos.nparams args_names) in
     let params = List.map mkVar param_names in
     let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in
     (* The bindings of the principle
@@ -611,7 +611,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       in
       (* in fact we must also add the parameters to the constructor args *)
       let constructor_args =
-	let params_id = fst (list_chop princ_infos.nparams args_names) in
+	let params_id = fst (List.chop princ_infos.nparams args_names) in
 	(List.map mkVar params_id)@(List.rev constructor_args)
       in
       (* We then get the constructor corresponding to this branch and
@@ -669,7 +669,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	g
     in
     (* end of branche proof *)
-    let param_names = fst (list_chop princ_infos.nparams args_names) in
+    let param_names = fst (List.chop princ_infos.nparams args_names) in
     let params = List.map mkVar param_names in
     let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in
     (* The bindings of the principle
@@ -996,7 +996,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
       ]
 	g
     in
-    let params_names = fst (list_chop princ_infos.nparams args_names) in
+    let params_names = fst (List.chop princ_infos.nparams args_names) in
     let params = List.map mkVar params_names in
     tclTHENSEQ
       [ tclMAP h_intro (args_names@[res;hres]);
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 4fe22a354..21c0d86a4 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -165,11 +165,11 @@ let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a =
       let res = f !i acc x in i := !i + 1; res)
     acc arr
 
-(* Like list_chop but except that [i] is the size of the suffix of [l]. *)
+(* Like List.chop but except that [i] is the size of the suffix of [l]. *)
 let list_chop_end i l =
   let size_prefix = List.length l -i in
   if size_prefix < 0 then failwith "list_chop_end"
-  else list_chop size_prefix l
+  else List.chop size_prefix l
 
 let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a =
   let i = ref 0 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 14d9b7fcb..8b0fc2739 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -705,7 +705,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
     (try
       (tclTHENS
 	 destruct_tac
-	 (list_map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
+	 (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
 	 ))
     with 
       | UserError("Refiner.thensn_tac3",_) 
@@ -1014,7 +1014,7 @@ let compute_terminate_type nb_args func =
 	  Array.of_list
 	    (lift 5 a_arrow_b:: mkRel 3::
 	       constr_of_global func::mkRel 1::
-	       List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
+	       List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
 	    )
 	 )
   in
@@ -1044,7 +1044,7 @@ let termination_proof_header is_mes input_type ids args_id relation
       let nargs = List.length args_id in
       let pre_rec_args =
 	List.rev_map
-	  mkVar (fst (list_chop (rec_arg_num - 1) args_id))
+	  mkVar (fst (List.chop (rec_arg_num - 1) args_id))
       in
       let relation = substl pre_rec_args relation in
       let input_type = substl pre_rec_args input_type in
@@ -1297,7 +1297,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 		    (Elim.h_decompose_and (mkVar hid))
 		    (fun g ->
 		       let ids' = pf_ids_of_hyps g in
-		       lid := List.rev (list_subtract ids' ids);
+		       lid := List.rev (List.subtract ids' ids);
 		       if !lid = [] then lid := [hid];
 		       tclIDTAC g
 		    )
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index e0b27a2f5..94b79503a 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -214,7 +214,7 @@ let ppcm_mon m m' =
 let repr p = p
 
 let equal =
-  Util.list_for_all2eq
+  Util.List.for_all2eq
     (fun (c1,m1) (c2,m2) -> P.equal c1 c2 && m1=m2)
 
 let hash p =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ed06d6e11..ccf397eda 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -153,7 +153,7 @@ let tag_hypothesis,tag_of_hyp, hyp_of_tag =
 let hide_constr,find_constr,clear_tables,dump_tables =
   let l = ref ([]:(constr * (identifier * identifier * bool)) list) in
   (fun h id eg b -> l := (h,(id,eg,b)):: !l),
-  (fun h -> try list_assoc_f eq_constr h !l with Not_found -> failwith "find_contr"),
+  (fun h -> try List.assoc_f eq_constr h !l with Not_found -> failwith "find_contr"),
   (fun () -> l := []),
   (fun () -> !l)
 
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 62c0dc4a9..ee341cbc2 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -26,7 +26,7 @@ let omega_tactic l =
        | "N" -> Tacinterp.interp <:tactic<zify_N>>
        | "Z" -> Tacinterp.interp <:tactic<zify_op>>
        | s -> Errors.error ("No Omega knowledge base for type "^s))
-    (Util.list_uniquize (List.sort compare l))
+    (Util.List.uniquize (List.sort compare l))
   in
   tclTHEN
     (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 98cad09e0..6abcc7b6f 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -352,11 +352,11 @@ let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 =
   let new_eq = List.hd (normalize new_eq) in
   let eliminated_var, def = chop_var var new_eq.body in
   let other_equations =
-    Util.list_map_append
+    Util.List.map_append
       (fun e ->
         normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in
   let inequations =
-    Util.list_map_append
+    Util.List.map_append
       (fun e ->
         normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in
   let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in
@@ -368,9 +368,9 @@ let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,
   if !debug then display_system print_var (e::other);
   try
     let v,def = chop_factor_1 e.body in
-    (Util.list_map_append
+    (Util.List.map_append
       (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other,
-     Util.list_map_append
+     Util.List.map_append
        (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs)
   with FACTOR1 ->
     eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs)
@@ -523,7 +523,7 @@ let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system =
     failwith "disequation in simplify";
   clear_history ();
   List.iter (fun e -> add_event (HYP e)) system;
-  let system = Util.list_map_append normalize system in
+  let system = Util.List.map_append normalize system in
   let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in
   let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in
   let system = (eqs @ simp_eq,simp_ineq) in
@@ -658,7 +658,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
     | ([],ineqs,expl_map) -> ineqs,expl_map
   in
   try
-    let system = Util.list_map_append normalize system in
+    let system = Util.List.map_append normalize system in
     let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in
     let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in
     let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
@@ -700,13 +700,13 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
         let s1,s2 =
           List.partition (fun (_,_,decomp,_) -> sign decomp) systems in
         let s1' =
-	  List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in
+	  List.map (fun (dep,ro,dc,pa) -> (Util.List.except id dep,ro,dc,pa)) s1 in
         let s2' =
-	  List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in
+	  List.map (fun (dep,ro,dc,pa) -> (Util.List.except id dep,ro,dc,pa)) s2 in
         let (r1,relie1) = solve s1'
 	and (r2,relie2) = solve s2' in
 	let (eq,id1,id2) = List.assoc id explode_map in
-	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2
+	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.List.union relie1 relie2
       with FULL_SOLUTION (x0,x1) -> (x0,x1)
     in
     let act,relie_on = solve all_solutions in
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index a548d4d4a..5a843e2b7 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -19,7 +19,7 @@ let romega_tactic l =
        | "N" -> Tacinterp.interp <:tactic<zify_N>>
        | "Z" -> Tacinterp.interp <:tactic<zify_op>>
        | s -> Errors.error ("No ROmega knowledge base for type "^s))
-    (Util.list_uniquize (List.sort compare l))
+    (Util.List.uniquize (List.sort compare l))
   in
   tclTHEN
     (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 50031052b..6c6e2c57f 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -220,7 +220,7 @@ let unintern_omega env id =
    calcul des variables utiles. *)
 
 let add_reified_atom t env =
-  try list_index0_f Term.eq_constr t env.terms
+  try List.index0_f Term.eq_constr t env.terms
   with Not_found ->
     let i = List.length env.terms in
     env.terms <- env.terms @ [t]; i
@@ -231,7 +231,7 @@ let get_reified_atom env =
 (* \subsection{Gestion de l'environnement de proposition pour Omega} *)
 (* ajout d'une proposition *)
 let add_prop env t =
-  try list_index0_f Term.eq_constr t env.props
+  try List.index0_f Term.eq_constr t env.props
   with Not_found ->
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
@@ -412,7 +412,7 @@ pour faire des opérations de normalisation sur les équations.  *)
 (* Extraction des variables d'une équation. *)
 (* Chaque fonction retourne une liste triée sans redondance *)
 
-let (@@) = list_merge_uniq compare
+let (@@) = List.merge_uniq compare
 
 let rec vars_of_formula = function
   | Oint _ -> []
@@ -812,7 +812,7 @@ let destructurate_hyps syst =
       (i,t) :: l ->
 	let l_syst1 = destructurate_pos_hyp i []  [] t in
 	let l_syst2 = loop l in
-	list_cartesian (@) l_syst1 l_syst2
+	List.cartesian (@) l_syst1 l_syst2
     | [] -> [[]] in
   loop syst
 
@@ -912,13 +912,13 @@ let add_stated_equations env tree =
 
 (* PL: experimentally, the result order of the following function seems
    _very_ crucial for efficiency. No idea why. Do not remove the List.rev
-   or modify the current semantics of Util.list_union (some elements of first
+   or modify the current semantics of Util.List.union (some elements of first
    arg, then second arg), unless you know what you're doing. *)
 
 let rec get_eclatement env = function
     i :: r ->
       let l = try (get_equation env i).e_depends with Not_found -> [] in
-      list_union (List.rev l) (get_eclatement env r)
+      List.union (List.rev l) (get_eclatement env r)
   | [] -> []
 
 let select_smaller l =
@@ -1031,7 +1031,7 @@ let mk_direction_list l =
 (* \section{Rejouer l'historique} *)
 
 let get_hyp env_hyp i =
-  try list_index0 (CCEqua i) env_hyp
+  try List.index0 (CCEqua i) env_hyp
   with Not_found -> failwith (Printf.sprintf "get_hyp %d" i)
 
 let replay_history env env_hyp =
@@ -1198,8 +1198,8 @@ let resolution env full_reified_goal systems_list =
   let useful_equa_id = equas_of_solution_tree solution_tree in
   (* recupere explicitement ces equations *)
   let equations = List.map (get_equation env) useful_equa_id in
-  let l_hyps' = list_uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in
-  let l_hyps = id_concl :: list_remove id_concl l_hyps' in
+  let l_hyps' = List.uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in
+  let l_hyps = id_concl :: List.remove id_concl l_hyps' in
   let useful_hyps =
     List.map (fun id -> List.assoc id full_reified_goal) l_hyps in
   let useful_vars =
@@ -1253,7 +1253,7 @@ let resolution env full_reified_goal systems_list =
       |	((O_left | O_mono) :: l) -> app coq_p_left [| loop l |]
       |	(O_right :: l) -> app coq_p_right [| loop l |] in
     let correct_index =
-      let i = list_index0 e.e_origin.o_hyp l_hyps in
+      let i = List.index0 e.e_origin.o_hyp l_hyps in
       (* PL: it seems that additionnally introduced hyps are in the way during
              normalization, hence this index shifting... *)
       if i=0 then 0 else Pervasives.(+) i (List.length to_introduce)
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index f540349ed..f838b56c6 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -87,7 +87,7 @@ let interp_map l c =
   with Not_found -> None
 
 let interp_map l t =
-  try Some(list_assoc_f eq_constr t l) with Not_found -> None
+  try Some(List.assoc_f eq_constr t l) with Not_found -> None
 
 let protect_maps = ref Stringmap.empty
 let add_map s m = protect_maps := Stringmap.add s m !protect_maps
@@ -194,7 +194,7 @@ let dummy_goal env =
    Evd.sigma = sigma}
 
 let exec_tactic env n f args =
-  let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in
+  let lid = List.tabulate(fun i -> id_of_string("x"^string_of_int i)) n in
   let res = ref [||] in
   let get_res ist =
     let l = List.map (fun id ->  List.assoc id ist.lfun) lid in
@@ -834,7 +834,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
-    [ let (t,lr) = list_sep_last lrt in ring_lookup f lH lr t]
+    [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t]
 END
 
 
@@ -1162,5 +1162,5 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl =
 
 TACTIC EXTEND field_lookup
 | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
-      [ let (t,l) = list_sep_last lt in field_lookup f lH l t ]
+      [ let (t,l) = List.sep_last lt in field_lookup f lH l t ]
 END